Fri 17 Jun 2022 15:50 - 16:10 at Macaw - Refinement Types Chair(s): Sorav Bansal

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 \textbf{RefinedC}, which combines \emph{ownership types} (for modular reasoning about shared state and concurrency) with \emph{refinement types} (for encoding precise invariants on C data types and Hoare-style specifications for C functions).

RefinedC is both \emph{automated} (requiring minimal user intervention) and \emph{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 \textbf{Lithium}. By restricting to a carefully chosen (yet still expressive) fragment of separation logic, Lithium supports predictable, automatic, goal-directed proof search \emph{without backtracking}. We demonstrate the effectiveness of RefinedC on a range of representative examples of idiomatic C code.

https://dl.acm.org/doi/10.1145/3453483.3454036
this URL might only work when visiting from a https://dl.acm.org/doi/10.1145/3453483.3454036 URL.

Fri 17 Jun

Displayed time zone: Pacific Time (US & Canada) change

15:30 - 16:50
Refinement TypesSIGPLAN Track at Macaw
Chair(s): Sorav Bansal IIT Delhi and CompilerAI Labs
15:30
20m
Talk
(OOPSLA 2020) Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell
SIGPLAN Track
Yiyun Liu University of Maryland at College Park, James Parker Galois, Inc., Patrick Redmond University of California at Santa Cruz, Lindsey Kuper University of California at Santa Cruz, Michael Hicks University of Maryland at College Park, Niki Vazou IMDEA Software Institute
15:50
20m
Talk
(PLDI 2021) RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types
SIGPLAN Track
Michael Sammler MPI-SWS, Rodolphe Lepigre MPI-SWS, Robbert Krebbers Radboud University Nijmegen, Kayvan Memarian University of Cambridge, Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS
Link to publication DOI Authorizer link Pre-print
16:10
20m
Talk
(POPL 2021) Data Flow Refinement Type Inference
SIGPLAN Track
Zvonimir Pavlinovic Google, USA, Yusen Su University of Waterloo, Thomas Wies New York University
16:30
20m
Talk
(PLDI 2021) RbSyn: type- and effect-guided program synthesis
SIGPLAN Track
Sankha Narayan Guria University of Maryland, College Park, Jeffrey S. Foster Tufts University, David Van Horn University of Maryland
Link to publication DOI Authorizer link Pre-print