| 研究課題/領域番号 |
19K20245
|
|---|
| 研究種目 |
若手研究
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
森口 草介 東京工業大学, 情報理工学院, 助教 (60733409)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2025-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
3,510千円 (直接経費: 2,700千円、間接経費: 810千円)
2021年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2020年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2019年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
|
|---|
| キーワード | 定理証明支援系 / メタプログラミング / 形式検証 / 関数リアクティブプログラミング / 型システム / プログラム意味論 / プログラム検証 / 対話的証明支援系 |
|---|
| 研究開始時の研究の概要 |
本研究では、ソースコードを入出力の対象とするプログラムの検証手法を提案し、検証システムが実現できることを実証する。プログラムが意図通りに動作することを確かめるプログラム検証手法が多く提案されているが、検証するプログラムが利用するデータは数値が主である。本研究の対象とするプログラムは、他のプログラムの構築を助けたり、プログラムの分析をするものであり、本研究での検証により一般に開発されるプログラムの信頼性の向上が期待できる。
|
| 研究実績の概要 |
2023年度は直接本課題の成果を外部に発表する機会はなかったが、いくつかの進捗が得られた。
メタプログラミングの側面としては、関数リアクティブプログラミング言語に対して時間の決定および分散システムへの応用を提案しているが、これをメタレベルの計算として行う仕組みについて検討している。
一方、検証の側面としては、データフロープログラミング言語に対する可逆計算のモデルとして作られた、部分関数を含むリスト計算についての定式化と、その無限リストへの展開を行っている。一般に無限リストは同一性を通常のリストのように行うことはできず、また定理証明支援系の体系では計算途中の失敗を全体の失敗とすることができない。これは、データフロープログラミング言語においてメタプログラミングを行うモジュールを無限に延長した場合に、大きな制限となることが予想される。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
メタレベルへの検証の適用が進んでおらず、検証システムの構築としては遅れている。
実際の検証を行うための情報は集まっているため、本年度の達成目標とする。
|
| 今後の研究の推進方策 |
定理証明支援系Coqを用い、簡易な言語によるメタレベルとベースレベルの実現、およびその上での検証を行う。
また、高階の検証が可能なライブラリIRISを用い、C言語を対象とした検証を試行する。
|
