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 条

[31] Formal specification and implementation of an automated pattern-based parallel-code generation framework
Gervasio Pérez
Sergio Yovine
International Journal on Software Tools for Technology Transfer, 2019, 21 : 183 - 202
[32] Formal specification and implementation of an automated pattern-based parallel-code generation framework
Perez, Gervasio
Yovine, Sergio
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2019, 21 (02) : 183 - 202
[33] Correctness issues of UML Class and State Machine Models in the C# Code Generation and Execution Framework
Derezinska, Anna
Pilitowski, Romuald
2008 INTERNATIONAL MULTICONFERENCE ON COMPUTER SCIENCE AND INFORMATION TECHNOLOGY (IMCSIT), VOLS 1 AND 2, 2008, : 474 - 481
[34] Cn-continuity in Digital Image Correlation: Implementation and Validation of C-1, C0 and C1 Algorithms
Wittevrongel, L.
Lava, P.
Lomov, S. V.
Debruyne, D.
STRAIN, 2015, 51 (06) : 444 - 458
[35] Towards Automatic Code Generation of Run-Time Power Management for Embedded Systems using Formal Methods
Fathabadi, Asieh Salehi
Maeda-Nunez, Luis Alfonso
Butler, Michael J.
Al-Hashimi, Bashir M.
Merrett, Geoff V.
2015 IEEE 9TH INTERNATIONAL SYMPOSIUM ON EMBEDDED MULTICORE/MANYCORE SYSTEMS-ON-CHIP (MCSOC), 2015, : 104 - 111
[36] A new form of the hypersingular boundary integral equation for 3-D acoustics and its implementation with C0 boundary elements
Liu, YJ
Chen, SH
COMPUTER METHODS IN APPLIED MECHANICS AND ENGINEERING, 1999, 173 (3-4) : 375 - 386
[37] A methodology for automatic generation, formal verification and implementation of safe PLC programs for power supply equipment of the electric lines of railway control systems
Niang, M.
Riera, B.
Philippot, A.
Zaytoon, J.
Gellot, F.
Coupat, R.
COMPUTERS IN INDUSTRY, 2020, 123
[38] An inf-sup approach to C0\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$C_0$$\end{document}-semigroup generation for an interactive composite structure-Stokes PDE dynamics
Pelin G. Geredeli
Journal of Evolution Equations, 2024, 24 (3)
[39] A new generation criterion theorem for C0\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$C_0$$\end{document}-semigroups implying a generalization of Kaiser–Weis–Batty’s perturbation theorem
Hatem Megdiche
Semigroup Forum, 2023, 107 (2) : 491 - 524
[40] On the monotonicity and discrete maximum principle of the finite difference implementation of C0\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$C^0$$\end{document}-Q2\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$Q^2$$\end{document} finite element method
Hao Li
Xiangxiong Zhang
Numerische Mathematik, 2020, 145 (2) : 437 - 472

← 1 2 3 4 →