A mechanically verified compiling specification for a realistic compiler

vts_5349.pdf (633.6Kb)
67 Seiten
67 Seiten
Veröffentlichung
2005-09-05Authors
Dold, Axel
Henke, Friedrich Wilhelm von
Vialard, Vincent
Goerigk, Wolfgang
Arbeitspapier
Faculties
Fakultät für InformatikSeries
Ulmer Informatik-Berichte
Abstract
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.
Date created
2002
Subject headings
[LCSH]: Compilers (Computer programs)Metadata
Show full item recordDOI & citation
Please use this identifier to cite or link to this item: 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
Citation formatter >