An Executable Formal Semantics of C with Applications

被引：43
|
作者：
Ellison, Chucky [1 ]
Rosu, Grigore [1 ]
机构：
[1] Univ Illinois, Chicago, IL 60680 USA
来源：
ACM SIGPLAN NOTICES | 2012年 / 47卷 / 01期
关键词：
Languages; Standardization; Verification; REWRITING LOGIC;
D O I：
10.1145/2103621.2103719
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
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.
引用
收藏
页码：533 / 544
页数：12
相关论文
共 50 条
  • [1] An Executable Formal Semantics of C with Applications
    Ellison, Chucky
    Rosu, Grigore
    [J]. POPL 12: PROCEEDINGS OF THE 39TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2012, : 533 - 544
  • [2] An Executable Formal Semantics of PHP
    Filaretti, Daniele
    Maffeis, Sergio
    [J]. ECOOP 2014 - OBJECT-ORIENTED PROGRAMMING, 2014, 8586 : 567 - 592
  • [3] KRust: A Formal Executable Semantics of Rust
    Wang, Feng
    Song, Fu
    Zhang, Min
    Zhu, Xiaoran
    Zhang, Jun
    [J]. PROCEEDINGS 2018 12TH INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE 2018), 2018, : 44 - 51
  • [4] Executable Formal Semantics for the POSIX Shell
    Greenberg, Michael
    Blatt, Austin J.
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2020, 4 (POPL):
  • [5] A Formal Framework for Prototyping Executable Semantics in ATL
    Boronat, Artur
    [J]. THEORY AND PRACTICE OF MODEL TRANSFORMATION, ICMT 2018, 2018, 10888 : 157 - 172
  • [6] An executable formal semantics for UML-RT
    Posse, Ernesto
    Dingel, Juergen
    [J]. SOFTWARE AND SYSTEMS MODELING, 2016, 15 (01): : 179 - 217
  • [7] A formal executable semantics of the Java']JavaCard platform
    Barthe, G
    Dufay, G
    Jakubiec, L
    Serpette, B
    de Sousa, SM
    [J]. PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, 2001, 2028 : 302 - 319
  • [8] Formal executable semantics for conformance in the MDE framework
    Egea, Marina
    Rusu, Vlad
    [J]. INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2010, 6 (1-2) : 73 - 81
  • [9] An executable formal semantics for UML-RT
    Ernesto Posse
    Juergen Dingel
    [J]. Software & Systems Modeling, 2016, 15 : 179 - 217
  • [10] Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny
    Cassez, Franck
    Fuller, Joanne
    Ghale, Milad K.
    Pearce, David J.
    Quiles, Horacio M. A.
    [J]. FORMAL METHODS, FM 2023, 2023, 14000 : 571 - 583
12345