Formally Verified Compilation in the Context of Functional Safety
形式検証されたコンパイラと機能安全への運用
- Delivery
- Available on this site
- Format
- Price
- Non-members (tax incl.)：￥1,100 Members (tax incl.)：￥880
- Publication code
- 20265031
- Paper/Info type
- Proceedings (Spring)
No.7-26
- Pages
- 1-8(Total 8 p)
- Date of publication
- May 2026
- Publisher
- JSAE
- Language
- English
- Event
- 2026 JSAE Annual Congress (Spring)
Detailed Information
| Author(J) | 1) Daniel Kästner, 2) Bernhard Schommer, 3) Alexander Rogovskyy, 4) Michael Schmidt, 5) Adrian Dapprich |
|---|---|
| Author(E) | 1) Daniel Kästner, 2) Bernhard Schommer, 3) Alexander Rogovskyy, 4) Michael Schmidt, 5) Adrian Dapprich |
| Affiliation(J) | 1) AbsInt, 2) AbsInt, 3) AbsInt, 4) AbsInt, 5) AbsInt |
| Affiliation(E) | 1) AbsInt, 2) AbsInt, 3) AbsInt, 4) AbsInt, 5) AbsInt |
| Abstract(J) | CompCertは，誤コンパイルから解放されていることが，数学的証明を用いて形式的に検証されたコンパイラです．本発表ではコンパイラの設計と証明について概説し，TriCore向けにサイズとパフォーマンスに関する実験データを提示します．ソフトウェア開発および検証プロセスの効率向上に向けた新規の取り組みを説明し，安全規格を準拠のための認証について議論します． Translation |
| Abstract(E) | CompCert is the first commercially available optimizing compiler that is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation. The executable code it produces is proved to behave exactly as specified by the semantics of the source C program. This presentation gives an overview of design and proof concept of CompCert, and gives experimental data about performance and size of the generated code on TriCore Aurix. We describe novel contributions to improve the efficiency of the software development and verification process, and discuss the tool qualification strategy with respect to current safety norms. |
