| 研究課題/領域番号 |
22K19766
|
|---|
| 研究種目 |
挑戦的研究(萌芽)
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
中区分60:情報科学、情報工学およびその関連分野
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
住井 英二郎 東北大学, 情報科学研究科, 教授 (00333550)
|
|---|
| 研究期間 (年度) |
2022-06-30 – 2025-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
6,500千円 (直接経費: 5,000千円、間接経費: 1,500千円)
2024年度: 520千円 (直接経費: 400千円、間接経費: 120千円)
2023年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2022年度: 5,200千円 (直接経費: 4,000千円、間接経費: 1,200千円)
|
|---|
| キーワード | プログラミング言語理論／プログラム理論 / 形式手法（フォーマルメソッド），計算モデル / セキュリティ型つきλ計算 / 非機密化，動的レベル生成 / 環境双模倣 |
|---|
| 研究開始時の研究の概要 |
広義の「計算」（情報処理）を記述する体系としての「プログラミング言語」理論（特に本研究代表者らが研究・構想中の、非機密化や動的レベル生成を含むセキュリティ型つきλ計算の環境双模倣）を、狭義の計算機プログラムだけでなく人間社会のシステム（特に計算機に限らない情報セキュリティ）に関する記述・推論(reasoning)・検証にも適用することを試み、それらの理論と応用を相互に発展させる。
|
| 研究実績の概要 |
以下を含む複数の研究を研究協力者らとともに、他の研究とも連携して行なった。
・与えられた二つの関数型プログラムの振る舞いが等しいことを、SMTソルバー（整数等の理論つき論理式の充足可能性（一種の真偽）を自動的に判定するプログラム）にもとづき自動的に検証する、等価性検証器に関する既存研究・実装を調査・評価した。その結果、ごく簡単な「一階」の（すなわち、関数自体ではなく単なる整数等を引数や戻り値とする）プログラムであっても、表面的・軽微な違いしかないプログラムであれば等価と判定できる場合も多いが、本質的なアルゴリズムどころかプログラミングスタイルが少し違うだけでもしばしば判定に失敗する（判定アルゴリズムが停止せずタイムアウト等する）ことがわかった。当研究代表者らによるプログラム等価性証明手法である「環境双模倣」は「高階」の（すなわち、関数自体を引数とする）プログラムを主な対象とするが、一階の場合も自明に含み、そのような場合はSMTソルバーを用いた自動化も比較的容易と思われるので、内部の計算ステップの違いを無視できる「up-to reduction」等の手法を適切に用いれば、前述のような問題点を改善できる可能性が高いと予想される。
プログラム等価性とその証明はシステム一般の検証においても重要となる性質・手法であり、広義の「計算」（情報処理）を記述する体系としての「プログラミング言語」理論を、狭義の計算機プログラムだけでなく幅広いシステムに関する記述・推論(reasoning)・検証にも適用することを試み、それらの理論と応用を相互に発展させるという本研究の目的に沿う結果である。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
前年度と同様の理由に加え、当年度は教育（学生指導）の負担も極めて大きかったが、改善の方向にある。
|
| 今後の研究の推進方策 |
バイアウト等の制度を活用して、引き続き研究時間の確保に最大限努力しつつ、遅れてはいるが当初の計画に沿って研究を遂行する。
|
