Write a Blog >>
PLDI 2021
Sun 20 - Sat 26 June 2021 PLDI

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 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 C code.

Conference Day
Thu 24 Jun

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

13:30 - 14:05
Talks 4B: Concurrency, Compilation, and DebuggingPLDI at PLDI-B +12h
13:30
5m
Talk
Mirror: Making Lock-Free Data Structures Persistent
PLDI
Michal FriedmanTechnion, Erez PetrankTechnion, Pedro RamalheteCisco Systems
DOI
13:35
5m
Talk
Fluid: A Framework for Approximate Concurrency via Controlled Dependency Relaxation
PLDI
Huaipan JiangPennsylvania State University, Haibo ZhangPennsylvania State University, Xulong TangUniversity of Pittsburgh, Vineetha GovindarajPennsylvania State University, Jack SampsonPennsylvania State University, Mahmut Taylan KandemirPennsylvania State University, Danfeng ZhangPennsylvania State University
DOI
13:40
5m
Talk
Frequent Background Polling on a Shared Thread, using Light-Weight Compiler Interrupts
PLDI
Nilanjana BasuUniversity of Illinois at Chicago, Claudio MontanariUniversity of Illinois at Chicago, Jakob ErikssonUniversity of Illinois at Chicago
DOI
13:45
5m
Talk
Alive2: Bounded Translation Validation for LLVM
PLDI
Nuno P. LopesMicrosoft Research, Juneyoung LeeSeoul National University, Chung-Kil HurSeoul National University, Zhengyang LiuUniversity of Utah, John RegehrUniversity of Utah
DOI Pre-print
13:50
5m
Talk
Incremental Whole-Program Analysis in Datalog with Lattices
PLDI
Tamás SzabóJGU Mainz; Workday, Sebastian ErdwegJGU Mainz, Gábor BergmannBudapest University of Technology and Economics; IncQuery Labs
DOI
13:55
5m
Talk
Logical Bytecode Reduction
PLDI
Christian Gram KalhaugeUniversity of California at Los Angeles; Technical University of Denmark, Jens PalsbergUniversity of California at Los Angeles
DOI
14:00
5m
Talk
RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types
PLDI
Michael SammlerMPI-SWS, Rodolphe LepigreMPI-SWS, Robbert KrebbersRadboud University Nijmegen, Kayvan MemarianUniversity of Cambridge, Derek DreyerMPI-SWS, Deepak GargMPI-SWS
DOI

Conference Day
Fri 25 Jun

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

01:30 - 02:05
Talks 4B: Concurrency, Compilation, and DebuggingPLDI at PLDI-B
01:30
5m
Talk
Mirror: Making Lock-Free Data Structures Persistent
PLDI
Michal FriedmanTechnion, Erez PetrankTechnion, Pedro RamalheteCisco Systems
DOI
01:35
5m
Talk
Fluid: A Framework for Approximate Concurrency via Controlled Dependency Relaxation
PLDI
Huaipan JiangPennsylvania State University, Haibo ZhangPennsylvania State University, Xulong TangUniversity of Pittsburgh, Vineetha GovindarajPennsylvania State University, Jack SampsonPennsylvania State University, Mahmut Taylan KandemirPennsylvania State University, Danfeng ZhangPennsylvania State University
DOI
01:40
5m
Talk
Frequent Background Polling on a Shared Thread, using Light-Weight Compiler Interrupts
PLDI
Nilanjana BasuUniversity of Illinois at Chicago, Claudio MontanariUniversity of Illinois at Chicago, Jakob ErikssonUniversity of Illinois at Chicago
DOI
01:45
5m
Talk
Alive2: Bounded Translation Validation for LLVM
PLDI
Nuno P. LopesMicrosoft Research, Juneyoung LeeSeoul National University, Chung-Kil HurSeoul National University, Zhengyang LiuUniversity of Utah, John RegehrUniversity of Utah
DOI Pre-print
01:50
5m
Talk
Incremental Whole-Program Analysis in Datalog with Lattices
PLDI
Tamás SzabóJGU Mainz; Workday, Sebastian ErdwegJGU Mainz, Gábor BergmannBudapest University of Technology and Economics; IncQuery Labs
DOI
01:55
5m
Talk
Logical Bytecode Reduction
PLDI
Christian Gram KalhaugeUniversity of California at Los Angeles; Technical University of Denmark, Jens PalsbergUniversity of California at Los Angeles
DOI
02:00
5m
Talk
RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types
PLDI
Michael SammlerMPI-SWS, Rodolphe LepigreMPI-SWS, Robbert KrebbersRadboud University Nijmegen, Kayvan MemarianUniversity of Cambridge, Derek DreyerMPI-SWS, Deepak GargMPI-SWS
DOI