PLDI 2019 (series) / DeepSpec 2019 (series) / DeepSpec 2019 /
Refinement-Based Game Semantics for CompCert
In recent years, formal verification of computer systems of increasing size has become practical. Researchers have been able to verify complex artifacts at a variety of abstraction levels spanning from CPU designs to network protocols. These achievements remain discrete efforts, but there has been increasing interest in rendering them interoperable, as exemplified by the DeepSpec project. The ability to connect correctness proofs of components verified at various levels of abstraction would enable the construction of extremely reliable heterogenous systems through end-to-end verification. In this talk, we propose that a successful synthesis of existing research on game semantics, refinement-based methods, abstraction layers and logical relations has the potential to serve as a common theory of certified components. We apply this methodology to define a compositional semantics for the verified compiler CompCert, and demonstrate that the compiler's correctness proof can be extended to this compositional setting much more easily than using previous approaches.
Sun 23 Jun
|14:00 - 14:45|
Ben LaurieGoogle Research
|14:45 - 15:15|
Jérémie KoenigYale University