An executable formal semantics of C with applications

Chucky Ellison; Grigore Rosu

doi:10.1145/2103621.2103719

An executable formal semantics of C with applications

Chucky Ellison
, Grigore Rosu

Research output: Contribution to journal › Article › peer-review

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 language	English (US)
Pages (from-to)	533-544
Number of pages	12
Journal	ACM SIGPLAN Notices
Volume	47
Issue number	1
DOIs	https://doi.org/10.1145/2103621.2103719
State	Published - Jan 2012

ASJC Scopus subject areas

General Computer Science

Online availability

10.1145/2103621.2103719

Library availability

Discover UIUC Full Text

Cite this

@article{124cab86fa654950a8563cde9c77b1be,

title = "An executable formal semantics of C with applications",

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.",

author = "Chucky Ellison and Grigore Rosu",

year = "2012",

month = jan,

doi = "10.1145/2103621.2103719",

language = "English (US)",

volume = "47",

pages = "533--544",

journal = "ACM SIGPLAN Notices",

issn = "1523-2867",

publisher = "Association for Computing Machinery",

number = "1",

}

TY - JOUR

T1 - An executable formal semantics of C with applications

AU - Ellison, Chucky

AU - Rosu, Grigore

PY - 2012/1

Y1 - 2012/1

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/84857188920

UR - https://www.scopus.com/pages/publications/84857188920#tab=citedBy

U2 - 10.1145/2103621.2103719

DO - 10.1145/2103621.2103719

M3 - Article

AN - SCOPUS:84857188920

SN - 1523-2867

VL - 47

SP - 533

EP - 544

JO - ACM SIGPLAN Notices

JF - ACM SIGPLAN Notices

IS - 1

ER -

An executable formal semantics of C with applications

Abstract

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this