Sie können Bookmarks mittels Listen verwalten, loggen Sie sich dafür bitte in Ihr SLUB Benutzerkonto ein.
Medientyp:
E-Artikel
Titel:
An executable formal semantics of C with applications
Beteiligte:
Ellison, Chucky;
Rosu, Grigore
Erschienen:
Association for Computing Machinery (ACM), 2012
Erschienen in:
ACM SIGPLAN Notices, 47 (2012) 1, Seite 533-544
Sprache:
Englisch
DOI:
10.1145/2103621.2103719
ISSN:
0362-1340;
1558-1160
Entstehung:
Anmerkungen:
Beschreibung:
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.