2023 Fiscal Year Annual Research Report
Theory and Application for Robust and High-Performance Systems Programming Languages
| Project/Area Number |
22KJ0561
|
|---|
| Allocation Type | Multi-year Fund |
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
松下 祐介 東京大学, 情報理工学系研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2023-03-08 – 2024-03-31
|
| Keywords | プログラム検証 / 分離論理 / Iris / Coq |
|---|
| Outline of Annual Research Achievements |
3年間の研究期間にわたって、Rust の所有権型システム、および RustHorn の預言にもとづく検証手法を核として、特に、システムプログラムの検証について分離論理による基礎づけを与える、RustHornBelt や Nola といった研究プロジェクトを進めた。
2023年度は、主に Nola に取り組んだ。これは、分離論理（ヒープメモリなどについてスケーラブルに検証するための論理）において共有された可変な状態について論じるための「不変条件」や「借用」といった仕組みを、「共有対象を記述する命題の表現と解釈についてパラメトライズする」ことで柔軟に実現する、新しいアプローチを提案するものである。特に、Iris 分離論理フレームワークのライブラリとして定理証明支援系 Coq で機械化し、一般の検証プロジェクトで使えるようにした。これらの成果をまとめた博士論文 "Non-Step-Indexed Separation Logic with Invariants and Rust-Style Borrows" を執筆・12月に提出し、審査に合格し、3月に博士号を得た。
9月には、スイス ETH Zurich の Peter Muller 教授・Ralf Jung 助教のグループを現地訪問し、自らの研究プロジェクト・今後の研究について1時間ほどのトークをし、さらに1週間ほどにわたり、グループのメンバーと研究について幅広く議論した。
また、研究室の後輩である中山崇氏の研究プロジェクトについても、素朴な手法の問題点の指摘・提案手法の正しさの証明・論文執筆などで貢献し、その成果をまとめた論文 "Borrowable Fractional Ownership Types for Verification" が国際会議 VMCAI 2024 に採択され、1月に出版された。
|
