• English
    • Deutsch
  • English 
    • English
    • Deutsch
  • Login
View Item 
  •   Home
  • Universität Ulm
  • Publikationen
  • View Item
  •   Home
  • Universität Ulm
  • Publikationen
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

A mechanically verified compiling specification for a realistic compiler

Thumbnail
vts_5349.pdf (633.6Kb)
67 Seiten
Veröffentlichung
2005-09-05
Authors
Dold, Axel
Henke, Friedrich Wilhelm von
Vialard, Vincent
Goerigk, Wolfgang
Arbeitspapier


Faculties
Fakultät für Informatik
Series
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)
License
Standard (Fassung vom 03.05.2003)
https://oparu.uni-ulm.de/xmlui/license_v1

Metadata
Show full item record

DOI & 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 >



Policy | kiz service OPARU | Contact Us
Impressum | Privacy statement
 

 

Advanced Search

Browse

All of OPARUCommunities & CollectionsPersonsInstitutionsPublication typesUlm SerialsDewey Decimal ClassesEU projects UlmDFG projects UlmOther projects Ulm

My Account

LoginRegister

Statistics

View Usage Statistics

Policy | kiz service OPARU | Contact Us
Impressum | Privacy statement