RefinedC: automating the foundational verification of C code with refined ownership types
Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg
Abstract
Given the central role that C continues to play in systems software, and the difficulty of writing safe and correct C code, it remains a grand challenge to develop effective formal methods for verifying C programs. In this paper, we propose a new approach to this problem: a type system we call RefinedC, which combines ownership types (for modular reasoning about shared state and concurrency) with refinement types (for encoding precise invariants on C data types and Hoare-style specifications for C functions).
Topics & Concepts
Computer scienceProgramming languageConcurrencyAbstract data typeModular designSeparation logicHoare logicCode (set theory)Data typeTheoretical computer scienceSoftware engineeringCorrectnessSet (abstract data type)Security and Verification in ComputingLogic, programming, and type systemsDistributed systems and fault tolerance