Theory and Application for Robust and High-Performance Systems Programming Languages

鲁棒高性能系统编程语言的理论与应用

• 批准号: 22KJ0561
• 负责人: 松下 祐介
• 金额: $ 1.41万
• 依托单位: The University of Tokyo
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for JSPS Fellows
• 财政年份: 2023
• 资助国家: 日本
• 起止时间: 2023-03-08 至 2024-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22KJ0561/
• 关键词: Rust; プログラム検証; 分離論理; システムプログラミング

トップ国際会議 ACM PLDI 2022 に前年度に条件付きで採択された主著論文 "RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code"（松下、Denis、Jourdan、Dreyer）について、論文およびアーティファクト（ソースコード等）の最終版を提出し、論文の最終的な採択・アーティファクトの再利用可能性評価を得て、正式に出版した。さらに、論文の上位約1割にのみ与えられる Distinguished Paper Award を受賞した。この論文は、RustHorn（松下ら、2020）で提案された、Rust の所有権型と預言（未来の情報の先取り）の手法を利用して Rust プログラムを効率よく検証する手法の正当性を、様々な API を含む Rust の広いサブセットに対し一般に証明するための枠組みを提案し、定理証明支援系 Coq と分離論理フレームワーク Iris で機械化して実証した、というものである。そして、アメリカ・サンディエゴで開催された国際会議 ACM PLDI 2022 に現地参加し、コロナ禍で長らく難しかった世界の研究者たちとの対面による密な交流を果たし、主著論文 "RustHornBelt" について口頭で発表・議論した。また、世界の最新の研究動向について知見を得て、自分の研究についても知ってもらえるように働きかけた。東京大学大学院理学系研究科・理学部ニュース 2022年5月号 の「理学のススメ」に単著で一般向けの研究紹介記事「ソフトウェアの世界を切り拓く」を寄稿した。この記事では、研究分野の背景、研究という営みに対して抱いている思い、RustHorn のアイデアなどについて書いている。

主要作者论文《RustHornBelt: A Semantic Foundation for Function Verification of Rust Programs with Unsafe Code》（Matsushita、Denis、Jourdan、Dreyer）于去年在国际顶级会议 ACM PLDI 2022 上有条件接受了最终版本。提交源代码（源代码等），论文最终被接受，工件经过可重用性评估，正式发布。此外，他还获得了杰出论文奖，该奖项仅颁发给前 10% 的论文。本文检验了 RustHorn（Matsushita 等人，2020）中提出的方法的有效性，该方法使用 Rust 的所有权类型和预言（预测未来信息）方法来有效地验证 Rust 程序，他为 Rust 的广泛子集提出了一个通用证明框架，包括 API，并通过使用 Coq（定理证明支持系统）和 Iris（解耦逻辑框架）对其进行机械化来进行演示。随后，他参加了在美国圣地亚哥举行的国际会议ACM PLDI 2022，与来自世界各地的研究人员进行了近距离的面对面交流，并给予了长期以来因冠状病毒大流行而难以实现的机会。关于他的主要论文“RustHornBelt”的口头陈述。·讨论。我还努力了解世界各地最新的研究趋势，并帮助人们了解我自己的研究。他在东京大学研究生院理学院/理学院2022年5月号的《科学推荐》上发表了一篇面向公众的单人研究介绍文章“开放软件世界”消息。在这篇文章中，我写了我的研究领域背景、我的研究想法以及我对 RustHorn 的想法。

项目成果

RustHorn: CHC-based Verification for Rust Programs

RustHorn：基于 CHC 的 Rust 程序验证

• DOI: 10.1145/3462205
• 发表时间: 2021
• 期刊: ACM Transactions on Programming Languages and Systems
• 影响因子: 1.3
• 作者: Matsushita Yusuke;Tsukada Takeshi;Kobayashi Naoki
• 通讯作者: Kobayashi Naoki

RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code

• DOI: 10.1145/3519939.3523704
• 发表时间: 2022-06
• 期刊: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
• 作者: Yusuke Matsushita;Xavier Denis;Jacques-Henri Jourdan;Derek Dreyer

MPI-SWS(ドイツ)

MPI-SWS（德国）