|||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.
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.