A Mechanically Verified Compiling Specification for a Lisp Compiler

  • Axel Dold
  • Vincent Vialard
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2245)


We report on an ongoing effort in mechanically proving correct a compiling specification for a 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 four steps through a series of intermediate languages. This paper focuses on the first phase, namely, the compilation of ComLisp to the stack-intermediate language SIL, where parameter passing is implemented by a stack technique. 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.


Abstract Syntax Source Language Correctness Property Target Architecture Abstract Data Type 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    E. Börger and W. Schulte. Defining the Java Virtual Machine as Platform for Provably Correct Java Compilation. In 23rd Int. Symposium on Mathematical Foundations of Computer Science, volume 1450 of LNCS. Springer, 1998.Google Scholar
  2. 2.
    M. Broy. Experiences with Software Specification and Verification using LP, the Larch Proof Assistant. Technical report, Digital Systems Research Center, 1992.Google Scholar
  3. 3.
    L.M. Chirica and D.F. Martin. Toward Compiler Implementation Correctness Proofs. ACM Transactions on Programming Languages and Systems, 8(2):185–214, April 1986.zbMATHCrossRefGoogle Scholar
  4. 4.
    Paul Curzon. The Verified Compilation of Vista Programs. Internal Report, Computer Laboratory, University of Cambridge, January 1994.Google Scholar
  5. 5.
    Axel Dold. Formal Software Development using Generic Development Steps. Logos-Verlag, Berlin, 2000. Dissertation, Universität Ulm.Google Scholar
  6. 6.
    W. Goerigk, A. Dold, T. Gaul, G. Goos, A. Heberle, F. von Henke, U. Hoffmann, H. Langmaack, H. Pfeifer, H. Ruess, and W. Zimmermann. Compiler Correctness and Implementation Verification: The Verifix Approach. In Proceedings of the Poster Session of CC’96-International Conference on Compiler Construction. ida, 1996. TR-Nr.: R-96-12.Google Scholar
  7. 7.
    Wolfgang Goerigk, Thilo Gaul, and Wolf Zimmermann. Correct Programs without Proof? On Checker-Based Program Verification. In Proceedings ATOOLS’98 Workshop on “Tool Support for System Specification, Development, and Verification”, Advances in Computing Science, Malente, 1998. Springer Verlag.Google Scholar
  8. 8.
    Wolfgang Goerigk and H. Langmaack. Compiler Implementation Verification and Trojan Horses. In D. Bainov, editor, Proc. of the 9th Int. Colloquium on Numerical Analysis and Computer Sciences with Applications, Plovdiv, Bulgaria, 2000.Google Scholar
  9. 9.
    G. Goos and W. Zimmermann. Verification of Compilers. In B. Steffen E.-R. Olderog, editor, Correct System Design, volume 1710 of LNCS, pages 201–230. Springer-Verlag, 1999.CrossRefGoogle Scholar
  10. 10.
    J. D. Guttman, L. G. Monk, J. D. Ramsdell, W. M. Farmer, and V. Swarup. A Guide to VLISP, A Verified Programming Language Implementation. Technical Report M92B091, The MITRE Corporation, Bedford, MA, September 1992.Google Scholar
  11. 11.
    Ulrich Hoffmann. Compiler Implementation Verification through Rigorous Syntactical Code Inspection. PhD thesis, Technische Fakultät der Christian-Albrechts-Universität zu Kiel, Kiel, 1998.Google Scholar
  12. 12.
    J.J. Joyce. A Verified Compiler for a Verified Microprocessor. Technical Report 167, University of Cambridge, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, England, March 1989.Google Scholar
  13. 13.
    J. McCarthy and J.A. Painter. Correctness of a Compiler for Arithmetical Expressions. In J.T. Schwartz, editor, Proceedings of a Symposium in Applied Mathematics, 19, Mathematical Aspects of Computer Science. American Mathematical Society, 1967.Google Scholar
  14. 14.
    J S. Moore. A Mechanically Verified Language Implementation. Journal of Automated Reasoning, 5(4), 1989.Google Scholar
  15. 15.
    Markus Müller-Olm. Modular Compiler Verification, volume 1283 of LNCS. Springer Verlag, Berlin, Heidelberg, New York, 1997. PhD Thesis.Google Scholar
  16. 16.
    S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, February 1995.CrossRefGoogle Scholar
  17. 17.
    W. Polak. Compiler Specification and Verification, volume 124 of LNCS. Springer-Verlag, 1981.zbMATHGoogle Scholar
  18. 18.
    Gerhard Schellhorn. Verifikation abstrakter Zustandsmaschinen. PhD thesis, Unversität Ulm, 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Axel Dold
    • 1
  • Vincent Vialard
    • 1
  1. 1.Fakultät für InformatikUniversität UlmUlmGermany

Personalised recommendations