Program Transformation and Compilation

This chapter consists of two parts: The first describes how to interleave symbolic execution with partial evaluation to render the representation of proof trees more compact. Besides saving proof effort, it helps a human user to navigate and comprehend a given proof situation better. The second part is about verifiably correct compilation. Instead of verifying a compiler, we use the verification engine of KeY to prove for a given program on the fly that it is correctly compiled through a sound program transformation. Program behavior of the source code is provably preserved at the level of the target language: source and compiled program terminate in states in which the values of a user-specified region of the heap are equivalent. We give a proof-of-concept of the approach in realizing a partial evaluator, i.e., a source-to-source compiler.

Authors and Affiliations

1. Technische Universität Darmstadt, Darmstadt, Germany

   Ran Ji & Richard Bubel

Corresponding author

Correspondence to Richard Bubel .

Editors and Affiliations

1. Chalmers University of Technology, Gothenburg, Sweden

   Wolfgang Ahrendt

2. Karlsruhe Institute of Technology (KIT), Karlsruhe, Baden-Württemberg, Germany

   Bernhard Beckert

3. Technische Universität Darmstadt, Darmstadt, Germany

   Richard Bubel

4. Technische Universität Darmstadt, Darmstadt, Hessen, Germany

   Reiner Hähnle

5. Karlsruher Institut für Technologie (KIT), Karlsruhe, Germany

   Peter H. Schmitt

6. Karlsruher Institut für Technologie (KIT), Karlsruhe, Germany

   Mattias Ulbrich

Reprints and permissions

© 2016 Springer International Publishing AG

Policies and ethics