形式検証されたコンパイラと機能安全への運用
Formally Verified Compilation in the Context of Functional Safety
- 提供方法
- 本サイト上にてダウンロード・閲覧可
- 形態
- 価格
- 一般価格(税込)：￥1,100 会員価格(税込)：￥880
- 文献番号
- 20265031
- 文献・情報種別
- 学術講演会予稿集（春）
No.7-26
- 掲載ページ
- 1-8(Total 8 p)
- 発行年月
- 2026年 5月
- 出版社
- (公社)自動車技術会
- 言語
- 英語
- イベント
- 2026年春季大会
書誌事項
| 著者 | 1) Daniel Kästner, 2) Bernhard Schommer, 3) Alexander Rogovskyy, 4) Michael Schmidt, 5) Adrian Dapprich |
|---|---|
| 著者（英） | 1) Daniel Kästner, 2) Bernhard Schommer, 3) Alexander Rogovskyy, 4) Michael Schmidt, 5) Adrian Dapprich |
| 勤務先 | 1) AbsInt, 2) AbsInt, 3) AbsInt, 4) AbsInt, 5) AbsInt |
| 勤務先（英） | 1) AbsInt, 2) AbsInt, 3) AbsInt, 4) AbsInt, 5) AbsInt |
| 抄録 | CompCertは，誤コンパイルから解放されていることが，数学的証明を用いて形式的に検証されたコンパイラです．本発表ではコンパイラの設計と証明について概説し，TriCore向けにサイズとパフォーマンスに関する実験データを提示します．ソフトウェア開発および検証プロセスの効率向上に向けた新規の取り組みを説明し，安全規格を準拠のための認証について議論します． |
| 抄録（英） | 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. 翻訳 |
