Files in this item

FilesDescriptionFormat

application/pdf

application/pdfellison-rosu-2010-tr.pdf (591Kb)
Main ArticlePDF

text/csv

text/csvresults.csv (27Kb)
Correctness resultsCSV file

text/csv

text/csvcoverage.csv (185Kb)
Coverage resultsCSV file

Description

Title:A Formal Semantics of C with Applications: Technical Report
Author(s):Ellison, Chucky M.; Roşu, Grigore
Subject(s):C
specification
semantics
executable semantics
formal semantics
C programming language
evaluation order
static analysis
dynamic analysis
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.
Issue Date:2011-11-22
Citation Info:@techreport{ellison-rosu-2010-tr, author = "Chucky Ellison and Grigore Ro{\c s}u", institution={University of Illinois}, number={ http://hdl.handle.net/2142/17414}, title = "A Formal Semantics of {C} with Applications", month = "November", year = "2010", }
Genre:Technical Report
Type:Text
Language:English
URI:http://hdl.handle.net/2142/17414
Publication Status:unpublished
Peer Reviewed:not peer reviewed
Date Available in IDEALS:2010-11-23


This item appears in the following Collection(s)

Item Statistics

  • Total Downloads: 394
  • Downloads this Month: 5
  • Downloads Today: 0