Towards the formal verification of a C0 compiler: Code generation and implementation correctness

被引：23
|
作者：
Leinenbach, D [1 ]
Paul, W [1 ]
Petrova, E [1 ]
机构：
[1] Univ Saarland, Dept Comp Sci, D-66123 Saarbrucken, Germany
来源：
SEFM 2005: THIRD IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS | 2005年
关键词：
D O I：
10.1109/SEFM.2005.51
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
In the spirit of the famous CLI stack project [2] the Verisoft project [31] aims at the pervasive verification of entire computer systems including hardware, system software, compiler, and communicating applications, with a special focus on industrial applications. The main programming language used in the Verisoft project is CO (a subset of C which is similar to MISRA C [20]). This paper reports on (i) an operational small steps semantics for CO which is formalized in Isabelle/HOL [25], (ii) the formal specification of a compiler from CO to the DLX machine language [14,23] in Isabelle/HOL, (iii) a paper and pencil correctness proof for this compiler and the status of the formal verification effort for this proof and (iv) the implementation of the compiler in CO and a formal proof in Isabelle/HOL that the implementation produces the same code as the specification.
引用
下载
收藏
页码：2 / 11
页数：10
相关论文
共 40 条
  • [21] Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL
    Blech, Jan Olaf
    Glesner, Sabine
    Leitner, Johannes
    Muelling, Steffen
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 141 (02) : 33 - 51
  • [22] An efficient RTL-based code generation for specified DSP C-compiler
    Pan, QH
    Liu, P
    Shi, C
    Yao, QD
    Zhu, SB
    Yan, L
    Zhou, Y
    Huang, WB
    MEDIA PROCESSORS 2002, 2002, 4674 : 141 - 149
  • [23] INFINITE TENSOR PRODUCTS OF C0(R): TOWARDS A GROUP ALGEBRA FOR R(N)
    Grundling, Hendrik
    Neeb, Karl-Hermann
    JOURNAL OF OPERATOR THEORY, 2013, 70 (02) : 311 - 353
  • [24] Design and implementation of the decompiler for virtual machine code of the C++ compiler in the ubiquitous game platform
    Lee, YangSun
    Kim, YoungKeun
    Kwon, HyeokJu
    ADVANCES IN HYBRID INFORMATION TECHNOLOGY, 2007, 4413 : 511 - 521
  • [25] Don't Sweat the Small Stuff Formal Verification of C Code Without the Pain
    Greenaway, David
    Lim, Japheth
    Andronick, June
    Klein, Gerwin
    ACM SIGPLAN NOTICES, 2014, 49 (06) : 429 - 439
  • [26] Formal verification of C systems code : SSStructured types, separation logic and theorem proving
    Sydney Research Lab., National ICT Australia, Eveleigh, Australia
    J Autom Reasoning, 2009, 2-4 (125-187):
  • [27] On the monotonicity and discrete maximum principle of the finite difference implementation of C0 finite element method
    Li, Hao
    Zhang, Xiangxiong
    NUMERISCHE MATHEMATIK, 2020, 145 (02) : 437 - 472
  • [28] Towards verification of C programs. C-light language and its formal semantics
    Nepomnyashchij, V.A.
    Anureev, I.S.
    Mikhajlov, I.N.
    Promskij, A.V.
    2002, Nauka Moscow (28):
  • [29] Towards Verification of C Programs. C-Light Language and Its Formal Semantics
    V. A. Nepomniaschy
    I. S. Anureev
    I. N. Mikhailov
    A. V. Promskii
    Programming and Computer Software, 2002, 28 : 314 - 323
  • [30] Towards verification of C programs. C-light language and its formal semantics
    Nepomniaschy, VA
    Anureev, IS
    Mikhailov, IN
    Promskii, AV
    PROGRAMMING AND COMPUTER SOFTWARE, 2002, 28 (06) : 314 - 323
1234