Formal Verification of a Java Compiler in Isabelle

  • Martin Strecker
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2392)


This paper reports on the formal proof of correctness of a compiler from a substantial subset of Java source language to Java bytecode in the proof environment Isabelle. This work is based on extensive previous formalizations of Java, which comprise all relevant features of object-orientation. We place particular emphasis on describing the effects of design decisions in these formalizations on the compiler correctness proof.


Operational Semantic Correctness Proof Program Counter Java Virtual Machine Type Safety 
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. [BN00]
    Stefan Berghofer and Tobias Nipkow. Executing higher order logic. In Proc. TYPES Working Group Annual Meeting 2000, LNCS, 2000. Available from Scholar
  2. [Bou95]
    Samuel Boutin. Preuve de correction de la compilation de Mini-ML en code CAM dans le système d’aide à la démonstration COQ. Technical Report 2536, INRIA Rocquencourt, April 1995.Google Scholar
  3. [Cur93]
    Paul Curzon. A verified Vista implementation. Technical Report 311, University of Cambridge, Computer Laboratory, September 1993. Available from
  4. [DV01]
    A. Dold and V. Vialard. A mechanically verified compiling specification for a Lisp compiler. In Proc. FSTTCS 2001, December 2001.Google Scholar
  5. [KN02]
    Gerwin Klein and Tobias Nipkow. Verified bytecode verifiers. Theoretical Computer Science, 2002. to appear.Google Scholar
  6. [MBHY89]
    J.S. Moore, W.R. Bevier, W. A. Hunt, and W. D. Young. System verification. Special issue of J. of Automated Reasoning, 5(4), 1989.Google Scholar
  7. [MW72]
    R. Milner and R. Weyhrauch. Proving compiler correctness in a mechanized logic. Machine Intelligence, 7:51–70, 1972.zbMATHGoogle Scholar
  8. [Nip01]
    Tobias Nipkow. Verified bytecode verifiers. In M. Miculan F. Honsell, editor, Foundations of Software Science and Computation Structures (FOS-SACS 2001), volume 2030 of Lecture Notes in Computer Science. Springer Verlag, 2001.CrossRefGoogle Scholar
  9. [NOP00]
    Tobias Nipkow, David von Oheimb, and Cornelia Pusch. μJava: Embedding a programming language in a theorem prover. In F.L. Bauer and R. Steinbrüggen, editors, Foundations of Secure Computation. Proc. Int. Summer School Marktoberdorf 1999, pages 117–144. IOS Press, 2000.Google Scholar
  10. [NPW02]
    Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL. A Proof Assistant for Higher-Order Logic. LNCS 2283. Springer, 2002.zbMATHGoogle Scholar
  11. [Ohe01a]
    David von Oheimb. Analyzing Java in Isabelle/HOL: Formalization, Type Safety and Hoare Logic. PhD thesis, Technische Universität München, 2001.
  12. [Ohe01b]
    David von Oheimb. Hoare logic for Java in Isabelle/HOL. Concurrency: Practice and Experience, 13(13), 2001.Google Scholar
  13. [Sch99]
    G. Schellhorn. Verifikation abstrakter Zustandsmaschinen. PhD thesis, Universität Ulm, 1999.Google Scholar
  14. [SSB01]
    R. Stärk, J. Schmid, and E. Börger. Java and the Java Virtual Machine-Definition, Verification, Validation. Springer Verlag, 2001.Google Scholar
  15. [Str02]
    Martin Strecker. Compilation and bytecode verification in μJava. Forthcoming, preprint available from, 2002.
  16. [You89]
    William D. Young. A mechanically verified code generator. J. of Automated Reasoning, 5(4):493–518, 1989.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Martin Strecker
    • 1
  1. 1.Fakultät für InformatikTechnische Universität MünchenGermany

Personalised recommendations