2012/01/18 by Chucky Ellison, Grigore Rosu, Grigore Roşu
Computer Science · #Advanced Malware Detection Techniques #Logic, programming, and type systems #Security and Verification in Computing
paper · doi:10.1145/2103621.2103719
openalex publication_date 2012/01/18 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/29
This paper describes an executable formal semantics of C. Being executable, the semantics has been thoroughly tested against the GCC torture test suite and successfully passes 99.2% of 776 test programs. It is the most complete and thoroughly tested formal definition of C to date. The semantics yields an interpreter, debugger, state space search tool, and model checker "for free". The semantics is shown capable of automatically finding program errors, both statically and at runtime. It is also used to enumerate nondeterministic behavior.