- Abstract:
-
We present an execution semantics of the C programming language for use in the CerCo project. It is based on the small-step inductive semantics used by the CompCert verified compiler. We discuss the extensions required for our target architecture, porting the semantics to our choice of tool, Matita, providing an equivalent executable semantics and the validation of the semantics.
- Links To Paper
- 1st Link
- 2nd Link
- Bibtex format
- @Misc{EDI-INF-RR-1412,
- author = {
Brian Campbell
and Robert Pollack
},
- title = {Executable Formal Semantics of C},
- year = 2010,
- month = {Dec},
- url = {http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D3_1.pdf},
- }
|
