Mechanized Semantics for the Clight Subset of the C Language
- 24 July 2009
- journal article
- research article
- Published by Springer Science and Business Media LLC in Journal of Automated Reasoning
- Vol. 43 (3), 263-288
- https://doi.org/10.1007/s10817-009-9148-3
Abstract
No abstract availableKeywords
This publication has 27 references indexed in Scilit:
- Coinductive big-step operational semanticsInformation and Computation, 2009
- A Formal Model of Memory Peculiarities for the Verification of Low-Level Operating-System CodeElectronic Notes in Theoretical Computer Science, 2008
- Separation Logic Semantics for Communicating ProcessesElectronic Notes in Theoretical Computer Science, 2008
- The ant and the grasshopperACM SIGPLAN Notices, 2007
- A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract)Electronic Notes in Theoretical Computer Science, 2007
- A machine-checked model for a Java-like language, virtual machine, and compilerACM Transactions on Programming Languages and Systems, 2006
- A high-level modular definition of the semantics of C♯Theoretical Computer Science, 2005
- Safer language subsets: an overview and a case history, MISRA CInformation and Software Technology, 2004
- Towards Verification of C Programs: Axiomatic Semantics of the C-kernel LanguageProgramming and Computer Software, 2003
- Formalizing the safety of Java, the Java virtual machine, and Java cardACM Computing Surveys, 2001