Wed 26 Jun 2019 08:50 - 09:10 at 229AB - Verification I Chair(s): Chung-Kil Hur

Developing technology for building verified stacks, i.e., computer systems with comprehensive proofs of correctness, is one way the science of programming languages furthers the computing discipline. While there have been successful projects verifying complex, realistic system components, including compilers (software) and processors (hardware), to date these verification efforts have not been compatible to the point of enabling a single end-to-end correctness theorem about running a verified compiler on a verified processor.

In this paper we show how to extend the trustworthy development methodology of the CakeML project, including its verified compiler, with a connection to verified hardware. Our hardware target is Silver, a verified proof-of-concept processor that we introduce here. The result is an approach to producing verified stacks that scales to proving correctness, at the hardware level, of the execution of realistic software including compilers and proof checkers. Alongside our hardware-level theorems, we demonstrate feasibility by hosting and running our verified artefacts on an FPGA board.

Conference Day
Wed 26 Jun

Displayed time zone: Tijuana, Baja California change

08:30 - 09:30
Verification IPLDI Research Papers at 229AB
Chair(s): Chung-Kil HurSeoul National University
08:30
20m
Talk
Semantic Program Alignment for Equivalence Checking
PLDI Research Papers
Berkeley ChurchillStanford University, Oded PadonStanford University, Rahul SharmaMicrosoft Research, Alex AikenStanford University
Media Attached
08:50
20m
Talk
Verified Compilation on a Verified Processor
PLDI Research Papers
Andreas LööwChalmers University of Technology, Ramana KumarDeepMind, Yong Kiam TanCarnegie Mellon University, USA, Magnus O. MyreenChalmers University of Technology, Sweden, Michael NorrishData61 at CSIRO, Australia / Australian National University, Australia, Oskar AbrahamssonChalmers University of Technology, Sweden, Anthony FoxUniversity of Cambridge, UK
DOI Pre-print Media Attached
09:10
20m
Talk
Argosy: Verifying Layered Storage Systems with Recovery Refinement
PLDI Research Papers
Tej ChajedMassachusetts Institute of Technology, USA, Joseph TassarottiBoston College, M. Frans KaashoekMassachusetts Institute of Technology, USA, Nickolai ZeldovichMassachusetts Institute of Technology, USA
DOI Pre-print Media Attached