Sat 22 Jun 2019 15:00 - 15:30 at 106B - Modular Reasoning Chair(s): Benjamin C. Pierce
A natural target for formal methods has been correctness proofs of
systems that combine hardware and software components, which
indeed is one of the main goals of the DeepSpec effort.
Well-known examples in this space include the CLInc stack verified
by J Strother Moore and associates in the 1980s, with the
predecessor tools of ACL2.  That development wasn't particularly
modular, in the sense of supporting low-cost reconfiguration of
proofs to fit new stacks with significant component reuse from
past examples.  I will explain progress at MIT on interfacing
hardware and software proofs in more modular styles that are
popular today at conferences like PLDI.  The central interface
point is the formal semantics of the machine language, which can
be used to state proof obligations for both a processor and a
compiler.  We have developed simple prototypes of both, sufficient
to support basic Internet-of-things applications, and we are
working toward finishing the end-to-end correctness result. 

Sat 22 Jun

Displayed time zone: Tijuana, Baja California change

14:00 - 15:30
Modular ReasoningDeepSpec at 106B
Chair(s): Benjamin C. Pierce University of Pennsylvania
Abstraction, Subsumption, and Linking in VST
Lennart Beringer Princeton University, Andrew W. Appel Princeton
Compositional Verification of Preemptive OS Kernels with Temporal and Spatial Isolation
Mengqi Liu Yale University
Modular Correctness Proofs at the Hardware-Software Interface
Joonwon Choi Massachusetts Institute of Technology, USA