POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Fri 19 Jan 2024 15:50 - 16:10 at Turing Lecture - Mechanized Proofs Chair(s): Andrei Popescu

Verified compilation of open modules (i.e., modules whose functionality depends on other modules) provides a foundation for end-to-end verification of modular programs ubiquitous in contemporary software. However, despite intensive investigation in this topic for decades, the proposed approaches are still difficult to use in practice as they rely on assumptions about the internal working of compilers which make it difficult for external users to apply the verification results. We propose an approach to verified compositional compilation without such assumptions in the setting of verifying compilation of heterogeneous modules written in first-order languages supporting global memory and pointers. Our approach is based on the memory model of CompCert and a new discovery that a Kripke relation with a notion of memory protection can serve as a uniform and composable semantic interface for the compiler passes. By absorbing the rely-guarantee conditions on memory evolution for all compiler passes into this Kripke Memory Relation and by piggybacking requirements on compiler optimizations onto it, we get compositional correctness theorems for realistic optimizing compilers as refinements that directly relate native semantics of open modules and that are ignorant of intermediate compilation processes. Such direct refinements support all the compositionality and adequacy properties essential for verified compilation of open modules. We have applied this approach to the full compilation chain of CompCert with its Clight source language and demonstrated that our compiler correctness theorem is open to composition and intuitive to use with reduced verification complexity through end-to-end verification of non-trivial heterogeneous modules that may freely invoke each other (e.g., mutually recursively).

Fri 19 Jan

Displayed time zone: London change

15:10 - 16:30
Mechanized ProofsPOPL at Turing Lecture
Chair(s): Andrei Popescu University of Sheffield
15:10
20m
Talk
Mechanizing Refinement Types
POPL
Michael Borkowski University of California, San Diego, Niki Vazou IMDEA Software Institute, Ranjit Jhala University of California at San Diego
15:30
20m
Talk
VST-A: A Foundationally Sound Annotation Verifier
POPL
Litao Zhou Shanghai Jiao Tong University; University of Hong Kong, Jianxing Qin Shanghai Jiao Tong University, Qinshi Wang Princeton University, Andrew W. Appel Princeton University, Qinxiang Cao Shanghai Jiao Tong University
15:50
20m
Talk
Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules
POPL
Ling Zhang Shanghai Jiao Tong University, Yuting Wang Shanghai Jiao Tong University, Jinhua Wu Shanghai Jiao Tong University, Jérémie Koenig Yale University, Zhong Shao Yale University
Pre-print
16:10
20m
Talk
A Formalization of Core Why3 in Coq
POPL
Joshua M. Cohen Princeton University, Philip Johnson-Freyd Sandia National Laboratories