Construction of Correct Compilers

The aim of the VERIFIX project is the construction of mathematically correct compilers, which includes both the development of formal methods for specification and implementation of a compiler, and also the implementation of concrete compilers and development tools. Our approach is relevant for industrial purposes, because our constraints are very practical: To deal with practically relevant imperative languages and to push usability and efficiency to the foreground. The standard publication is JUCS
(See also the Verifix home page)

Participants

Department Head Prof. Gerhard Goos

Alumni Prof. Sabine Glesner Prof. Wolf Zimmermann Dr. Thilo Gaul Dr. Rubino Geiß Dr. Andreas Heberle

Partner Prof. Hans Langmaack Prof. Heinrich von Henke Dr. Axel Dold Dr. Wolfgang Goerigk Dr. Ulrich Hoffmann Vincent Vialard Andreas Wolf

Related Publications

		2000
		Goos, Zimmermann, Verifying Compilers and ASMs
		Goos, Zimmermann, ASMs for uniform description of multistep transformations
		Gaul, Zimmermann, Goerigk, Practical Construction of Correct Compiler Implementations by Runtime Result Verification
		1999
		Gaul, Heberle, Zimmermann, Goerigk, Construction of Verified Software Systems with Program-Checking: An Application To Compiler Back-Ends
		Goos, Zimmermann, Verification of Compilers
		Gaul, Schumacher, Advanced Generator Techniques for Embedded Compilers
		Heberle, Gaul, Zimmermann, Construction of Verified Compiler Front-Ends with Program-Checking
		1998
		Dold, Gaul, Vialard, Zimmermann, ASM-Based Mechanized Verification of Compiler Backends
		Gaul, Schumacher, Compiler Techniques for Fast Migration of Embedded Applications
		Heberle, Löwe, Trapp, Safe Reuse of Source to Intermediate Language Compilations
		Gaul, Goerigk, Zimmermann, Correct Programs without Proof? On Checker-Based Program Verification
		Dold, Gaul, Zimmermann, Mechanized Verification of Compiler Back-Ends
		Goerigk, Zimmermann, Gaul, Heberle, Hoffmann, Praktikable Konstruktion korrekter Übersetzer
		Boesler, Codeerzeugung aus Abhängigkeitsgraphen
		Heuzeroth, Spezifikation und Verifikation von standardisierten Transformationen am Beispiel der imperativen Sprache IS
		1997
		Gaul, Goos, Heberle, Zimmermann, Zur Konstruktion verifizierter Übersetzer
		Goos, Sather-K - The Language
		Gaul, Zimmermann, On the Construction of Correct Compiler Back-Ends: An ASM Approach