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.

Autoren

Alumni Prof. Sabine Glesner

Ex-Studenten Simone Forster Matthias Jäger