An executable formal semantics of C with applications

Chucky Ellison, Grigore Roşu

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationPOPL'12 - Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Pages533-544
Number of pages12
DOIs
StatePublished - Mar 12 2012
Event39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'12 - Philadelphia, PA, United States
Duration: Jan 25 2012 → Jan 27 2012

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566

Other

Other39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'12
CountryUnited States
CityPhiladelphia, PA
Period1/25/12 → 1/27/12

Keywords

  • Languages
  • Standardization
  • Verification

ASJC Scopus subject areas

  • Software

Access to Document

Fingerprint Dive into the research topics of 'An executable formal semantics of C with applications'. Together they form a unique fingerprint.

Cite this