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

deepspec-2019-papers
14:00 - 15:30: DeepSpec 2019 - Modular Reasoning at 106B
Chair(s): Benjamin C. PierceUniversity of Pennsylvania
deepspec-2019-papers14:00 - 14:30
Talk
Lennart BeringerPrinceton University, Andrew AppelPrinceton
deepspec-2019-papers14:30 - 15:00
Talk
Mengqi LiuYale University
deepspec-2019-papers15:00 - 15:30
Talk
Joonwon ChoiMassachusetts Institute of Technology, USA