direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments


A Program Result Checker for the Lexical Analysis of the GNU C Compiler
Zitatschlüssel glesner04a
Autor Sabine Glesner and Simone Forster and Matthias Jäger
Buchtitel Proceedings of the COCV-Workshop (Compiler Optimization meets Compiler Verification), 7th European Conferences on Theory and Practice of Software (ETAPS 2004)
Seiten 19 - 35
Jahr 2004
Adresse Barcelona, Spain
Jahrgang Vol. 132 (2005)
Monat Apr
Verlag Elsevier, Electronic Notes in Theoretical Computer Science (ENTCS)
Zusammenfassung In theory, program result checking has been established as a well-suited method to construct formally correct compiler frontends but it has never proved its practicality for real-life compilers. Such a proof is necessary to establish result checking as the method of choice to implement compilers correctly. We show that the lexical analysis of the GNU C compiler can be formally specified and checked within the theorem prover Isabelle/HOL utilizing program checking. Thereby we demonstrate that formal specification and verification techniques are able to handle real-life compilers.
Typ der Publikation Conference Article
Download Bibtex Eintrag

Zusatzinformationen / Extras


Schnellnavigation zur Seite über Nummerneingabe