| Project/Area Number |
22K19766
|
|---|
| Research Category |
Grant-in-Aid for Challenging Research (Exploratory)
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
Medium-sized Section 60:Information science, computer engineering, and related fields
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
住井 英二郎 東北大学, 情報科学研究科, 教授 (00333550)
|
|---|
| Project Period (FY) |
2022-06-30 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥6,500,000 (Direct Cost: ¥5,000,000、Indirect Cost: ¥1,500,000)
Fiscal Year 2024: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2023: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2022: ¥5,200,000 (Direct Cost: ¥4,000,000、Indirect Cost: ¥1,200,000)
|
|---|
| Keywords | プログラミング言語理論／プログラム理論 / 形式手法（フォーマルメソッド），計算モデル / セキュリティ型つきλ計算 / 非機密化，動的レベル生成 / 環境双模倣 |
|---|
| Outline of Research at the Start |
広義の「計算」（情報処理）を記述する体系としての「プログラミング言語」理論（特に本研究代表者らが研究・構想中の、非機密化や動的レベル生成を含むセキュリティ型つきλ計算の環境双模倣）を、狭義の計算機プログラムだけでなく人間社会のシステム（特に計算機に限らない情報セキュリティ）に関する記述・推論(reasoning)・検証にも適用することを試み、それらの理論と応用を相互に発展させる。
|
| Outline of Annual Research Achievements |
以下を含む複数の研究を研究協力者らとともに、他の研究とも連携して行なった。
・与えられた二つの関数型プログラムの振る舞いが等しいことを、SMTソルバー（整数等の理論つき論理式の充足可能性（一種の真偽）を自動的に判定するプログラム）にもとづき自動的に検証する、等価性検証器に関する既存研究・実装を調査・評価した。その結果、ごく簡単な「一階」の（すなわち、関数自体ではなく単なる整数等を引数や戻り値とする）プログラムであっても、表面的・軽微な違いしかないプログラムであれば等価と判定できる場合も多いが、本質的なアルゴリズムどころかプログラミングスタイルが少し違うだけでもしばしば判定に失敗する（判定アルゴリズムが停止せずタイムアウト等する）ことがわかった。当研究代表者らによるプログラム等価性証明手法である「環境双模倣」は「高階」の（すなわち、関数自体を引数とする）プログラムを主な対象とするが、一階の場合も自明に含み、そのような場合はSMTソルバーを用いた自動化も比較的容易と思われるので、内部の計算ステップの違いを無視できる「up-to reduction」等の手法を適切に用いれば、前述のような問題点を改善できる可能性が高いと予想される。
プログラム等価性とその証明はシステム一般の検証においても重要となる性質・手法であり、広義の「計算」（情報処理）を記述する体系としての「プログラミング言語」理論を、狭義の計算機プログラムだけでなく幅広いシステムに関する記述・推論(reasoning)・検証にも適用することを試み、それらの理論と応用を相互に発展させるという本研究の目的に沿う結果である。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
前年度と同様の理由に加え、当年度は教育（学生指導）の負担も極めて大きかったが、改善の方向にある。
|
| Strategy for Future Research Activity |
バイアウト等の制度を活用して、引き続き研究時間の確保に最大限努力しつつ、遅れてはいるが当初の計画に沿って研究を遂行する。
|
