Paper Info
Title
RefinedC: automating the foundational verification of C code with refined ownership types
Abstract
ABSTRACTGiven 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). RefinedC is both automated (requiring minimal user intervention) and foundational (producing a proof of program correctness in Coq), while at the same time handling a range of low-level programming idioms such as pointer arithmetic. In particular, following the approach of RustBelt, the soundness of the RefinedC type system is justified semantically by interpretation into the Coq-based Iris framework for higher-order concurrent separation logic. However, the typing rules of RefinedC are also designed to be encodable in a new “separation logic programming” language we call Lithium. By restricting to a carefully chosen (yet expressive) fragment of separation logic, Lithium supports predictable, automatic, goal-directed proof search without backtracking. We demonstrate the effectiveness of RefinedC on a range of representative examples of C code.
Year
DOI
Venue
2021
10.1145/3453483.3454036
Programming Language Design and Implementation
Keywords
DocType
Citations 
C programming language, separation logic, ownership types, refinement types, proof automation, Iris, Coq
Conference
2
PageRank 
References 
Authors
0.40
0
6
Name
Order
Citations
PageRank
Michael Sammler132.10
Rodolphe Lepigre240.76
Robbert Krebbers314117.35
Kayvan Memarian42017.84
Derek Dreyer554230.97
Deepak Garg658145.48