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
相关论文
共 34 条
  • [1] AHO AV, 1973, THEORY PARSING TRANS, V2
  • [2] Bevier W. R., 1989, Journal of Automated Reasoning, V5, P411
  • [3] Beyer S, 2003, LECT NOTES COMPUT SC, V2860, P51
  • [4] BEYER S, 2005, IN PRESS INT J SOFTW, V7
  • [5] Blech J. O., 2004, LECT NOTES INFORM, V51, P449
  • [6] BURSTALL RM, 1972, MACH INTELL, V7, P23
  • [7] CURZON P, 1994, 1 PROCOS WORK GROUP
  • [8] DALINGER I, 2005, IN PRESS LNCS
  • [9] de Roever W-P., 2001, Concurrency Verification: Introduction to Compositional and Noncompositional Proof Methods
  • [10] Dold A, 2001, LNCS, P144
1234