| 研究課題/領域番号 |
18K11160
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60010:情報学基礎論関連
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
西田 直樹 名古屋大学, 情報学研究科, 准教授 (00397449)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2023-03-31
|
| 研究課題ステータス |
完了 (2022年度)
|
| 配分額 *注記 |
4,420千円 (直接経費: 3,400千円、間接経費: 1,020千円)
2022年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2021年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2020年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2019年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2018年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
|
|---|
| キーワード | プログラム変換 / 制約付き書換え / プログラム検証 / 書換え帰納法 / 等価性 / 実行時エラー検証 / 全パス到達可能性 / 定理自動証明 / 計算モデル / 帰納法 / 到達可能性 / 項書換えシステム / 補題生成 |
|---|
| 研究成果の概要 |
本研究では，ポインタを扱わない命令型プログラム，特に，C言語プログラムやLLVM中間表現を論理制約付き項書換えシステムに変換し，書換え帰納法および全パス到達可能性証明系に基づくプログラム検証の枠組みを構築し，検証ツールを実装した．プログラムの等価性証明は帰納的定理に帰着して書換え帰納法により証明し，指定した実行時エラーの非発生は全パス到達可能性問題に帰着して余帰納法に基づく証明系により証明する．さらに書換え帰納法に基づく証明系と循環証明系の証明力を比較するために，特定の条件を満たす帰納的述語に関するシークエントの恒真性を証明する循環証明と書換え帰納法証明が互いに変換可能であることを示した．
|
| 研究成果の学術的意義や社会的意義 |
本研究では，書換え理論を実用プログラムに応用することをめざし，車載組込みシステムの検証に提案手法を応用することを試みた．この応用はこれまでにない試みであり，本研究の成果は書換え理論，特に制約付き書換えの実用性・有用性を示したと言える．さらに，これまでに研究されてきた多くの書換え理論の研究成果が提案手法を通じて応用できる可能性も示した．その観点から学術的意義だけでなく，社会的意義がある研究課題であることも示したと言える．
一方，全パス到達可能性を実行時エラーの非発生の証明に応用することも新しい試みであり，その有用性・実用性の観点から今後，さらに研究する価値がある課題であることを示した．
|
