Repository logo

CN: Verifying Systems C Code with Separation-Logic Refinement Types

Published version



Change log


Pulte, Christopher 
Makwana, Dhruv 
Sewell, Thomas 
Memarian, Kayvan 
Sewell, Peter 


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.



C, verification, separation logic, refinement types, pKVM, Android

Journal Title

Proceedings of the ACM on Programming Languages

Conference Name

Journal ISSN


Volume Title


Association for Computing Machinery (ACM)
European Commission Horizon 2020 (H2020) ERC (101002277)
European Research Council (789108)
a European Research Council (ERC) Consolidator Grant for the project “TypeFoundry”, funded under the European Union’s Horizon 2020 Framework Programme (grant agreement no. 101002277); a European Research Council (ERC) Advanced Grant “ELVER” under the European Union’s Horizon 2020 research and innovation programme (grant agreement no. 789108); an EPSRC Doctoral Training studentship; funding from Google Research
Is supplemented by: