Sun 23 Jun 2019 14:45 - 15:15 at 106B - Verifying All the Things Chair(s): Zhong Shao
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

deepspec-2019-papers
14:00 - 15:15: DeepSpec 2019 - Verifying All the Things at 106B
Chair(s): Zhong ShaoYale University
deepspec-2019-papers14:00 - 14:45
Talk
Ben LaurieGoogle Research
deepspec-2019-papers14:45 - 15:15
Talk
Jérémie KoenigYale University