| Project/Area Number |
19K20245
|
|---|
| Research Category |
Grant-in-Aid for Early-Career Scientists
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
森口 草介 東京工業大学, 情報理工学院, 助教 (60733409)
|
|---|
| Project Period (FY) |
2019-04-01 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥3,510,000 (Direct Cost: ¥2,700,000、Indirect Cost: ¥810,000)
Fiscal Year 2021: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2020: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2019: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
|
|---|
| Keywords | 定理証明支援系 / メタプログラミング / 形式検証 / 関数リアクティブプログラミング / 型システム / プログラム意味論 / プログラム検証 / 対話的証明支援系 |
|---|
| Outline of Research at the Start |
本研究では、ソースコードを入出力の対象とするプログラムの検証手法を提案し、検証システムが実現できることを実証する。プログラムが意図通りに動作することを確かめるプログラム検証手法が多く提案されているが、検証するプログラムが利用するデータは数値が主である。本研究の対象とするプログラムは、他のプログラムの構築を助けたり、プログラムの分析をするものであり、本研究での検証により一般に開発されるプログラムの信頼性の向上が期待できる。
|
| Outline of Annual Research Achievements |
2023年度は直接本課題の成果を外部に発表する機会はなかったが、いくつかの進捗が得られた。
メタプログラミングの側面としては、関数リアクティブプログラミング言語に対して時間の決定および分散システムへの応用を提案しているが、これをメタレベルの計算として行う仕組みについて検討している。
一方、検証の側面としては、データフロープログラミング言語に対する可逆計算のモデルとして作られた、部分関数を含むリスト計算についての定式化と、その無限リストへの展開を行っている。一般に無限リストは同一性を通常のリストのように行うことはできず、また定理証明支援系の体系では計算途中の失敗を全体の失敗とすることができない。これは、データフロープログラミング言語においてメタプログラミングを行うモジュールを無限に延長した場合に、大きな制限となることが予想される。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
メタレベルへの検証の適用が進んでおらず、検証システムの構築としては遅れている。
実際の検証を行うための情報は集まっているため、本年度の達成目標とする。
|
| Strategy for Future Research Activity |
定理証明支援系Coqを用い、簡易な言語によるメタレベルとベースレベルの実現、およびその上での検証を行う。
また、高階の検証が可能なライブラリIRISを用い、C言語を対象とした検証を試行する。
|
