Universitšt Karlsruhe
A Program Result Checker for the Lexical Analysis of the GNU C Compiler

Konferenzartikel

[1]Sabine Glesner, Simone Forster, Matthias Jäger, A Program Result Checker for the Lexical Analysis of the GNU C Compiler, Proceedings of the COCV-Workshop (Compiler Optimization meets Compiler Verification), 7th European Conferences on Theory and Practice of Software (ETAPS 2004), Elsevier, Electronic Notes in Theoretical Computer Science (ENTCS), April 2004.

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.

[Erzeuge bibTeX Eintrag]

Autoren

Alumni
Prof. Sabine Glesner
Ex-Studenten
Simone Forster
Matthias Jäger
Login
Links