topic.CN.bib

@comment{{This file has been generated by bib2bib 1.99}}

@comment{{Command line: bibtex2html-1.99-with-magiclink/bib2bib -c topic:"CN" -ob topic.CN.bib sewellbib2.bib}}

@inproceedings{2023-popl-cn,
  author = {Christopher Pulte and Dhruv C. Makwana and Thomas Sewell and Kayvan Memarian and Peter Sewell and Neel Krishnaswami},
  title = {{CN}: Verifying systems {C} code with separation-logic refinement types},
  optcrossref = {},
  optkey = {},
  conf = {POPL 2023},
  booktitle = {Proceedings of the 50th ACM SIGPLAN Symposium on Principles of Programming Languages},
  optbooktitle = {},
  year = {2023},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optpages = {},
  month = jan,
  optaddress = {},
  optorganization = {},
  optpublisher = {},
  optnote = {Conditionally accepted},
  note = {Proc. ACM Programming Languages 7, POPL, Article 1},
  optnote = {},
  optannote = {},
  doi = {10.1145/3571194},
  abstract = {Despite significant progress in the verification of hypervisors, operating systems, and compilers, and in verification tooling, there exists a wide gap between the approaches used in verification projects and conventional development of systems software. We see two main challenges in bringing these closer together: verification handling the complexity of code and semantics of conventional systems software, and verification usability. 

We describe an experiment in verification tool design aimed at addressing some aspects of both: we design and implement CN, a separation-logic refinement type system for C systems software, aimed at predictable proof automation, based on a realistic semantics of ISO C. CN reduces refinement typing to decidable propositional logic reasoning, uses first-class resources to support pointer aliasing and pointer arithmetic, features resource inference for iterated separating conjunction, and uses a novel syntactic restriction of ghost variables in specifications to guarantee their successful inference. We implement CN and formalise key aspects of the type system, including a soundness proof of type checking. To demonstrate the usability of CN we use it to verify a substantial component of Google's pKVM hypervisor for Android.
},
  optapollourl = {https://www.repository.cam.ac.uk/handle/1810/288588},
  pdf = {http://www.cl.cam.ac.uk/users/pes20/cn-draft.pdf},
  optsupplementarymaterial = {https://doi.org/10.5281/zenodo.5662349},
  topic = {CN},
  opttopictwo = {Cerberus},
  project = {https://www.cl.cam.ac.uk/~cp526/popl23.html},
  elver = {true},
  recent = {true}
}

@inproceedings{fulminate-popl2025,
  author = {Rini Banerjee and Kayvan Memarian and Dhruv Makwana and Christopher Pulte and Neel Krishnaswami and Peter Sewell},
  title = {Fulminate: Testing {CN} Separation-Logic Specifications in {C}},
  optcrossref = {},
  optkey = {},
  conf = {POPL 2025},
  booktitle = {Proceedings of the 52nd ACM SIGPLAN Symposium on Principles of Programming Languages (Proc. PACM Programming Languages 9, POPL)},
  optbooktitle = {},
  year = {2025},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optpages = {},
  month = jan,
  optaddress = {},
  optorganization = {},
  publisher = {ACM},
  doi = {10.1145/3704879},
  pdf = {http://www.cl.cam.ac.uk/users/pes20/cn-testing-popl2025.pdf},
  optnote = {},
  optannote = {},
  abstract = {Separation logic has become an important tool for formally capturing and reasoning about the ownership patterns of imperative programs, originally for paper proof, and now the foundation for industrial static analyses and multiple proof tools.  However, there has been very little work on program \emph{testing} of separation-logic specifications in concrete execution. At first sight, separation-logic formulas are hard to evaluate in reasonable time, with their implicit quantification over heap splittings, and other explicit existentials.

In this paper we observe that a restricted fragment of separation logic, adopted in the CN proof tool to enable predictable proof automation, also has a natural and readable \emph{computational} interpretation, that makes it practically usable in runtime testing.  We discuss various design issues and develop this as a C+CN source to C source translation, Fulminate. This adds checks -- including ownership checks and ownership transfer -- for C code annotated with CN pre- and post-conditions; we demonstrate this on nontrivial examples, including the allocator from a production hypervisor.  We formalise our runtime ownership testing scheme, showing (and proving) how its reified ghost state correctly captures ownership passing, in a semantics for a small C-like language.
},
  elver = {true},
  recent = {true},
  topic = {CN},
  opttopictwo = {Cerberus}
}