Files in this item

FilesDescriptionFormat

application/pdf

application/pdfellison-rosu-2011-tr-b.pdf (701kB)
main articlePDF

application/pdf

application/pdfellison-rosu-2011-tr.pdf (915kB)
to deletePDF

text/csv

text/csvcoverage.csv (66kB)
Coverage resultsCSV file

Description

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


This item appears in the following Collection(s)

Item Statistics