University of Ulm, Faculty of Computer Science, Dept. of Artificial Intelligence up: Verifix Project

A Mechanically Verified Compiling Specification for a Realistic Compiler

A. Dold, F. W. von Henke, V. Vialard, W. Goerigk

Technical Report UIB 03-02, Universität Ulm, Fakultät für Informatik, Dec. 2002


We report on a large formal verification effort in mechanically proving correct a compiling specification for a realistic bootstrap compiler from ComLisp (a subset of ANSI Common Lisp sufficiently expressive to serve as a compiler implementation language) to binary Transputer code using the PVS system. The compilation is carried out in five steps through a series of intermediate languages. In the first phase, ComLisp is translated into a stack intermediate language (SIL), where parameter passing is implemented by a stack technique. Expressions are transformed from a prefix notation into a postfix notation according to the stack principle. SIL is then compiled into Cint where the ComLisp data structures (s-expressions) and operators are implemented in linear integer memory using a run-time stack and a heap. These two steps are machine independent. In the compiler's backend, first control structures (loops, conditionals) of the intermediate language Cint are implemented by linear assembler code with relative jumps, the infinite memory model of Cint is realized on the finite Transputer memory, and the basic Cint statements for accessing the stack and heap are implemented by a sequence of assembler instructions. The fourth phase consists of the implementation of code instructions with large and negative word operands, while the last phase is concerned with the integration of the assembly program into the memory. The context of this work is the joint research effort Verifix aiming at developing methods for the construction of correct compilers for realistic programming languages and real target architectures.

 Online Copy

Available as komprimiertes Postscript (432 KB)

 BibTeX Entry
  author = "A. Dold and F. W. v. Henke and V. Vialard and W. Goerigk}",
  title = "{A Mechanically Verified Compiling Specification for a Realistic Compiler}",
  institution =  "Universit{\"a}t Ulm, Fakult{\"a}t f{\"u}r Informatik",
  year =         "2002",
  number =       "02-03",
  type = "Ulmer Informatik-Berichte"

Dept. of AI Homepage Research Help Mail to Webmaster FvH 2002-01-15