About this Computer Science article
A Program Result Checker for the Lexical Analysis of the GNU C Compiler by Sabine Glesner; Simone Forster; Matthias Jäger is a Computer Science article available to read on EtoBox.
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.
It is typically read by researchers, students, and practitioners in Computer Science.
- Author
- Sabine Glesner; Simone Forster; Matthias Jäger
- Publisher
- Elsevier Science; Elsevier ; Elsevier BV; Amsterdam: Elsevier BV (ISSN 1571-0661)
- Published
- 2005
- Language
- EN
- Field
- Computer Science (Physical Sciences)