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 のアイデアなどについて書いている。

ACM PLDI 2022 was held on condition that the main paper "RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code"(Panasonic, Denis, Jourdan, Dreyer) was submitted, the final version of the paper was presented, and the final paper was published. Today, the paper is about 1 cut and the Distinguished Paper Award is awarded. RustHorn (Panasonic, 2020) The method of obtaining information in the future includes the following steps: ACM PLDI 2022 was held in Beijing in 1998 and was attended by researchers from all over the world. The main paper was "RustHornBelt". The latest research trends in the world include knowledge and knowledge, and self-determination. "Science and Technology" in the May 2022 issue of Graduate School of Science, University of Tokyo The background of the research field, the research center, the research center, the RustHorn center, the research center, the RustHorn center.

项目成果

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（德国）