University of Illinois Urbana-Champaign

A Formal Semantics of C with Applications: Technical Report

Ellison, Chucky M.; Rosu, Grigore

Content Files
coverage.csv
ellison-rosu-2010-tr.pdf
results.csv

Permalink

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

Description

Title
A Formal Semantics of C with Applications: Technical Report
Author(s)
  • Ellison, Chucky M.
  • Rosu, Grigore
Issue Date
2011-11-22
Keyword(s)
  • C
  • specification
  • semantics
  • executable semantics
  • formal semantics
  • C programming language
  • evaluation order
  • static analysis
  • dynamic analysis
Date of Ingest
2010-11-23T00:05:22Z
Abstract
"This paper describes an executable formal semantics of C expressed using a formalism based on term rewriting. Being executable, the semantics has been thoroughly tested against the GCC torture test suite and successfully passes over 96% of 715 test programs. It is the most complete and thoroughly tested formal definition of C to date. The semantics yields an interpreter, debugger, and state space search tool ""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. These techniques together allow the tool to identify undefined programs."
Type of Resource
text
Genre of Resource
Technical Report
Language
en
Permalink
http://hdl.handle.net/2142/17414

Owning Collections

Research and Tech Reports - Computer Science PRIMARY