• English
    • Deutsch
  • Deutsch 
    • English
    • Deutsch
  • Einloggen
Dokumentanzeige 
  •   Startseite
  • Universität Ulm
  • Publikationen
  • Dokumentanzeige
  •   Startseite
  • Universität Ulm
  • Publikationen
  • Dokumentanzeige
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
Autoren
Dold, Axel
Henke, Friedrich Wilhelm von
Vialard, Vincent
Goerigk, Wolfgang
Arbeitspapier


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

Metadata
Zur Langanzeige

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



Leitlinien | kiz Service OPARU | Kontakt
Impressum | Datenschutzerklärung
 

 

Erweiterte Suche

Browsen

Gesamter BestandBereiche & SammlungenPersonenInstitutionenPublikationstypUlmer Reihen & ZeitschriftenDDC-SachgruppenEU-Projekte UlmDFG-Projekte UlmWeitere Projekte Ulm

Mein Benutzerkonto

EinloggenRegistrieren

Statistik

Benutzungsstatistik

Leitlinien | kiz Service OPARU | Kontakt
Impressum | Datenschutzerklärung