| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 10329285 | Electronic Notes in Theoretical Computer Science | 2005 | 17 Pages |
Abstract
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.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Sabine Glesner, Simone Forster, Matthias Jäger,