University of Illinois Urbana-Champaign

An Executable Formal Semantics of C with Applications: Technical Report

Ellison, Chucky M.; Rosu, Grigore

Content Files
coverage.csv
ellison-rosu-2011-tr-b.pdf
ellison-rosu-2011-tr.pdf

Permalink

https://hdl.handle.net/2142/25816

Description

Title
An Executable Formal Semantics of C with Applications: Technical Report
Author(s)
  • Ellison, Chucky M.
  • Rosu, Grigore
Issue Date
2011-07-17
Keyword(s)
  • C
  • semantics
  • dynamic analysis
  • evaluation order
Date of Ingest
2011-07-17T20:10:12Z
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 770 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."
Type of Resource
text
Genre of Resource
Technical Report
Language
en
Permalink
http://hdl.handle.net/2142/25816

Owning Collections

Research and Tech Reports - Computer Science PRIMARY