Paper Info
Title
Verified compilation on a verified processor
Abstract
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.
Year
DOI
Venue
2019
10.1145/3314221.3314622
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
Keywords
Field
DocType
compiler verification, hardware verification, program verification, verified stack
Compiler verification,Computer science,Trustworthiness,Correctness,Field-programmable gate array,Real-time computing,Compiler,Software,Mathematical proof,Embedded system
Conference
ISBN
Citations 
PageRank 
978-1-4503-6712-7
0
0.34
References 
Authors
0
7
Name
Order
Citations
PageRank
Andreas Lööw101.01
Ramana Kumar214113.56
Yong Kiam Tan310712.93
Magnus O. Myreen462135.67
Michael Norrish5109161.77
Oskar Abrahamsson611.73
Anthony Fox7462.32