A mechanically verified compiling specification for a realistic compiler

vts_5349.pdf (633.6Kb)
67 Seiten
67 Seiten
Veröffentlichung
2005-09-05Autoren
Dold, Axel
Henke, Friedrich Wilhelm von
Vialard, Vincent
Goerigk, Wolfgang
Arbeitspapier
Fakultäten
Fakultät für InformatikSchriftenreihe
Ulmer Informatik-Berichte
Zusammenfassung
We report on a large verification effort in constructing an initial fully trusted bootstrap compiler executable for a realistic system programming language and real target processor. The construction and verification process comprises three tasks: the verification of the compiling specification (a relation between abstract source and target programs) with respect to the language semantics and a realistic correctness criterion. Second, the implementation of this specification in the high-level source language following a transformational approach, and third, the construction of a binary executable written in the compilers target language. The focus of this report is on the first verification task. This proof has been completely mechanized using the PVS specification and verification system and is one of the largest case-studies in formal verification we are aware of.
Erstellung / Fertigstellung
2002
Schlagwörter
[LCSH]: Compilers (Computer programs)Metadata
Zur LanganzeigeDOI & Zitiervorlage
Nutzen Sie bitte diesen Identifier für Zitate & Links: http://dx.doi.org/10.18725/OPARU-334
Dold, Axel et al. (2005): A mechanically verified compiling specification for a realistic compiler. Open Access Repositorium der Universität Ulm und Technischen Hochschule Ulm. http://dx.doi.org/10.18725/OPARU-334
Verschiedene Zitierstile >