A Verified Compiler For A Structured Assembly Language
Paul Curzon · 2005
We describe the verification of a compiler for a subset of the Vista language: a structured assembly language for the Viper microprocessor. This proof has been mechanically checked using the HOL system. We consider how the compiler correctness theorem could be used to deduce safety and liveness properties of compiled code from theorems stating that these properties hold of the source code. We also show how secure compilation can be achieved using automated theorem proving techniques. 1 Introduction In this paper, we describe the verification of a compiler for a subset of the Vista language[10]. Our motivation for verifying the compiler is to allow us to infer properties about the code which is actually executed from properties we prove about Vista programs. Previous work on the formal verification of compilers has largely considered the compiler correctness theorem itself to be the ultimate goal. Consequently, little attention has been given to identifying the way in which the correc...