Project Members
Dr. Sabine Glesner, Dipl.-Inform. Jan Olaf Blech, Simone Forster,
Matthias Jäger, Michael Mai
Project Goals:
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.
In this project, we investigate if and how the lexical and syntactic 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.
Publications
- Sabine Glesner, Simone Forster, and Matthias Jäger: A Program
Result Checker for the Lexical Analysis of the GNU C Compiler. In
Proceedings of the COCV-Workshop (Compiler Optimization meets
Compiler Verification), 7th European Conferences on Theory and
Practice of Software (ETAPS 2004), Barcelona, Spain, April 2004,
accepted for publication in Electronic Notes in Theoretical Computer
Science (ENTCS).
Student Projects
- Simone Forster: Term Project (Studienarbeit) "Formale Verifikation der
syntaktischen Analyse des GCC-Compilers in Isabelle/HOL" (Formal
Verification of the Syntactic Analysis of the GCC Compiler in Isabelle/HOL
, Fakultät
für Informatik, Universität Karlsruhe, 2004, laufende Arbeit (current work).
This work is sponsored by the Landesstiftung Baden-Württemberg within
the Eliteförderprogramm für Postdoktoranden.
Back to Sabine's Homepage
Back to Homepage of Postdoc Project