---

Verifix (Verifying Compilers)

Erroneous and buggy software dramatically increases the cost of software development cycles, the maintenance phase and even minor bugs often spoil the confidence in a software system. Software testing is one method to improve software reliability but especially the correctness of safety critical software crucially depends on the correctness of the underlying software engineering tools.

Adequate software engineering methods, especially formal methods, are used to support the correct construction of programs in high level programming languages. Compilers are used to transform those programs into binary executable code on concrete hardware processors. Thus, compilers themselves are used as tools in the process of correct construction and implementation of software. The correctness of the entire process crucially depends on compiler correctness.

Verifix is a joint research effort of groups at the universities Karlsruhe (G. Goos, W. Zimmermann), Kiel (H. Langmaack, W. Goerigk), and Ulm (F.W. von Henke, A. Dold) funded by the DFG (German Research Council) since 1995. The project aims at developing innovative repeatable engineering methods for constructing verifying compilers

• for realistic, industrially applicable imperative and object-oriented source programming languages and
• real world target and host processors
• which, by mechanical proof support and a-posteriori and runtime result checking are rigorously verified as executable host machine programs
• and practically and industrially approved compiler architecture and construction methods
• generate efficient code that compares to unverified compilers.

Full compiler correctness comprises

• the correctness of the compiling specification (a relation between abstract source and target language programs) with respect to source and target language semantics ( compiling verification ) and
• the correctness of a compiler implementation ( compiler implementation verification ), i.e. the correct transformation of the compiling specification to machine code of the compiler host processor. The correctness of the implementation of a compiler program can be modularized into the correctness proofs of a compiler implementation in a high-level language and the final compiler executable.

Main Results

The main results and achievements of the Verifix project are as follows:

• the consideration and creation of a suitable notion of correctness which takes the finite resources of the target processors into account (see, e.g. [Mueller-Olm,Wolf99], [Goerigk,Langmaack01])

• verifying compilers can be constructed with classical approved compiler construction technology with the help of unverified compiler generators for the front-end and back-end (e.g. Lex, Yacc, BEG). (see, e.g. [Goos,Zimmermann99])

• the method of rigorous algorithmic and manual a-posteriori program checking and code inspection to ensure implementation correctness (see, e.g. [Goerigk,Gaul,Zimmermann98]). A program checker routine checks at compile time if the output of an unverified process is correctly constructed from the input. Verification of the checking algorithm is usually much easier than verifying the generated compiler pass or generator.

• the technique to master the construction of initial bootstrap compilers and to solve the problem of realistic machine level compiler implementation which has been open for a long time. In order not to have to write the verified parts of the compiler and the program checkers directly in machine code, such a fully verified and correctly implemented initial compiler is required to serve as a sound and trusted implementation basis. Verifix has constructed such an initial fully correct compiler executable transforming ComLisp, a subset of ANSI Common Lisp into binary Transputer code. ComLisp is expressive enough to serve both as the source and (high-level) implementation language of this compiler.
(see, e.g. [Goerigk,Hoffmann98], [Dold,Vialard01])
• the use of automated proof systems to support the different verification tasks of the project (see below).

Verifix @ Ulm

The emphasis of the work at Ulm is on the main formal aspects, i.e. on formalizing, structuring, and automating proofs for establishing correctness results about compiler phases. As a formal verification vehicle, the specification and verification system PVS has been chosen. In particular, the project results achieved at Ulm are as follows:

• a completely mechanically verified compiling specification for the initial ComLisp compiler.
  The compiler uses five subsequent passes including front end and code generation down to the Transputer. This formal mechanical verification case-study is so far, one of the largest one we are aware of: approx. 18,000 manual proof interactions have been necessary, and the effort took about 36 person-months. The verification of the first phase of the compiler is described in a conference paper . A paper presenting the verification of the other four phases will be available soon.
• the formal, transformational construction of a high-level compiler implementation.
  Starting from the (verified) compiling specification of the first phase, namely, the translation of ComLisp to the stack-intermediate language SIL, an implementation has been constructed formally by applying correctness-preserving software development steps. For this purpose, a unified framework for the formal treatment of the transformational software development process has been developed.
• specification and verification of a back-end program checker.
  The back-end or code generation phase of a compiler is often generated, for instance, by bottom-up rewrite system (BURS) code generation techniques. Using such a tool, code generation is specified by a conditional term or graph rewriting system, and rewrite rule schemata are applied to select and replace parts of basic blocks by efficient target processor instructions. Here, the checker verifies the result of a sophisticated labeling process of expression trees with instances of rewrite rule schemata. Necessary, declarative properties are proved correct for a PVS implementation of such a checker.
• verification of back-end specifications.
  Based on the operational semantics of a basic-block oriented intermediate language and the DEC-Alpha target processor PVS is used to mechanically verify a set of rewrite rule schemata. The operational semantics of the languages is specified by means of abstract state machines (ASM's). Recipes have been developed on how to formalize ASM-based language semantics in PVS. A specific PVS strategy enables an automatic verification of the rules. Several erroneous rules have been found.
• formal verification of local optimizations.
  A generic scheme has been developed to verify transformations for peephole optimizations which is applicable to a large class of machine architectures.
• encoding of major parts of domain theory
  Major parts of domain theory (fixed-point theory) has been formalized in PVS. They form the basis for accomplishing compiling correctness proofs based on denotational language semantics.
• mechanization of the semantics of imperative and functional language constructs.
  A uniform encoding in PVS of various kinds of semantics of imperative programming language constructs (denotational, predicate transformers, weakest liberal precondition semantics, axiomatic semantics (Hoare), continuation-style semantics, and natural semantics) has been developed.
• construction of a set of generic theories for compiling standard language constructs.
  A hierarchy of verified generic PVS theories for compiling standard imperative language constructs (assignments, standard control structures, procedures) is provided.
• development and implementation of efficient proof techniques.
  
  • support for symbolic simulation in PVS
  • development of efficient decision procedures for a special class of bitvectors
  • PVS proof support for refinement calculus proofs

Project Members

• Ulm: Prof. Friedrich W. von Henke, Dr. Axel Dold
  (former members: Stephan Pfab, Holger Pfeifer, Dr. Harald Ruess, Vincent Vialard)
• Kiel: Prof. Hans Langmaack, Dr. Wolfgang Goerigk
• Karlsruhe: Prof. Gerhard Goos, Prof. Wolf Zimmermann (now: University of Halle), Dr. Sabine Glesner, Rubino Geiss

• W. Zimmermann, A. Dold
  A Framework for Modelling the Semantics of Expression Evaluation with Abstract State Machines
  Proc. of the 9th International Workshop on Abstract State Machines (ASM 2003),
  Springer LNCS, to appear.

• A. Dold, F. W. von Henke, V. Vialard, W. Goerigk
  A Mechanically Verified Compiling Specification for a Realistic Compiler
  Technical Report UIB 03-02, Universität Ulm, Fakultät für Informatik, Dec. 2002
  

• A. Dold, V. Vialard
  A Mechanically Verified Bootstrap Compiler
  Proc. of Kolloquium Programmiersprachen und Grundlagen der Programmierung
  Technical report AIB-2001-11,
  RWTH Aachen, Department of Computer Science, December 2001.
  

• A. Dold, V. Vialard
  A Mechanically Verified Compiling Specification for a Lisp Compiler
  Proc. of the 21st Conference on
  Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2001),
  December 13-15, Bangalore, India.
  Springer LNCS 2245.
  

• A. Dold
  Formal Software Development using Generic Development Steps
  PhD thesis, Universität Ulm, 2000.

• A. Dold, V. Vialard
  Formal Verification of a Compiler Back-End Generic Checker Program
  Proceedings of the Andrei Ershov Third International Conference
  Perspectives of System Informatics (PSI'99),
  Novosibirsk, Akademgorodok, Russia, July 6 - 9, 1999.
  Springer LNCS, 1755.

• A. Dold, T. Gaul, V. Vialard, W. Zimmermann
  ASM-Based Mechanized Verification of Compiler Backends
  Proc. 5th International Workshop on Abstract State Machines,
  Magdeburg, Germany, September 21-22, 1998.
  

• A. Dold, T. Gaul, W. Zimmermann
  Mechanized Verification of Compiler Backends
  Proc. of the Internat. Workshop on Software Tools for Technology Transfer (STTT'98),
  Aalborg, Denmark, July 12-13, 1998.
  

• M. Stegmüller
  Formale Verifikation des DLX RISC-Prozessors: Eine Fallstudie basierend auf abstrakten Zustandsmaschinen
  Masters Thesis, University of Ulm, 1998.

• O. Möller
  Solving Bit-Vector Equations - A Decision Procedure for Hardware Verification
  Masters Thesis, University of Ulm, 1998.

• S. Pfab
  Efficient Abstract Interpretation of Formal Specifications and Its Interrelationship with Theorem Proving
  Masters Thesis, University of Ulm, 1998.

• A. Dold, F. W. von Henke, H. Pfeifer, H. Rueß
  Formal Verification of Transformations for Peephole Optimization
  Proc. of FME'97, Springer LNCS 1313, pp. 459 - 472, September 1997

• F. Bartels, A. Dold, F. W. v. Henke, H. Pfeifer, and H. Rueß
  Formalizing Fixed-Point Theory in PVS
  Technical report UIB 96-10, Universität Ulm, Fakultät für Informatik, Dec. 1996
  

• H. Pfeifer, A. Dold, F. W. v. Henke, and H. Rueß
  Mechanized Semantics of Imperative Programming Constructs
  Technical report UIB 96-11, Universität Ulm, Fakultät für Informatik, Dec. 1996
  

• A. Dold, F. W. von Henke, H. Pfeifer, H. Rueß
  Generic Compilation Schemes for Simple Programming Constructs
  Technical report UIB 96-12, Universität Ulm, Fakultät für Informatik, Dec. 1996
  (a revised version (Jan'99) is available here .)

• W. Goerigk, A. Dold, Th. Gaul, G. Goos, A. Heberle, F.W. von Henke, U. Hoffmann, H. Langmaack, H. Pfeifer, H. Rueß, and W. Zimmermann.
  Compiler Correctness and Implementation Verification: The Verifix Approach.
  In P. Fritzson (ed.) Proceedings of the Poster Session of CC '96 - International Conference on Compiler Construction, IDA Technical Report LiTH-IDA-R-96-12, Linkøping University, Sweden, April 1996.
  

• H. Pfeifer, A. Dold, F.W. von Henke, H. Ruess
  Modelling abstract views on the Transputer in PVS
  Verifix Report, Ulm 13.1, 1996.
• A. Dold
  A Formalization of the Normal Form Approach to Compilation
  Verifix Report, Ulm 9.1, 1996.
• H. Pfeifer, A. Dold, F.W. von Henke, H. Ruess
  Formal Specification of the Transputer Instruction Set in PVS
  Verifix Report, Ulm 8.2, 1996.
• A. Dold
  A Formal Representation of Abstract State Machines using PVS
  Verifix Report, Ulm 6.2, 1996 (revised version, July 1998).
• A. Dold
  Representing the Alpha Processor Family using PVS
  Verifix Report, Ulm 4.1, 1996
• H. Pfeifer, A. Dold, F.W. von Henke, H. Ruess
  Supporting Refinement Calculus Proofs in PVS
  Verifix Report, Ulm 3.1, 1996.

(a complete list of Verifix publications and technical reports can be found on the project homepage)