Advancement and Application of Type Theory for Improving Software Safety

提高软件安全性的类型论进展及应用

• 批准号: 20240001
• 负责人: KOBAYASHI Naoki
• 金额: $ 31.53万
• 依托单位: Tohoku University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (A)
• 财政年份: 2008
• 资助国家: 日本
• 起止时间: 2008 至 2010
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-20240001/
• 关键词: ソフトウェア検証; 型システム; 高階モデル検査; 資源使用法検証; プログラム解析; 型理論; 述語抽象化; メモリ使用法解析; モデル検査; 高階再帰スキーム; 資源使用法解析; ツリーオートマトン

This research project aimed to improve the reliability of computer software, by refining type-based program verification methods we have studied before, and also by inventing new program verification techniques. As the former study, we have constructed verification tools for C programs and cryptographic protocols. As the latter study, we have shown novel applications of higher-order model checking to program verification, and constructed the first higher-order model checker in the world.

该研究项目旨在通过改进我们之前研究过的基于类型的程序验证方法以及发明新的程序验证技术来提高计算机软件的可靠性。作为前一项研究，我们构建了C程序和密码协议的验证工具。作为后一项研究，我们展示了高阶模型检查在程序验证中的新颖应用，并构建了世界上第一个高阶模型检查器。

项目成果

Polymorphic Contracts

多态合约

• 发表时间: 2010
• 期刊: Proceedings of European Symposium on Programming (ESOP2011)
• 作者: Joao Filipe Belo;Michael Greenberg;Atsushi Igarashi;Benjamin C.Pierce
• 通讯作者: Benjamin C.Pierce

Recursion Schemes for Verification of Higher-Order Programs

用于验证高阶程序的递归方案

• 发表时间: 2009
• 期刊: Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on principles of Programming Languages (POPL 2009)
• 作者: Naoki Kobayashi;Types and Higher-Order
• 通讯作者: Types and Higher-Order

Substructural Type Systems for Program Analysis

用于程序分析的子结构类型系统

• 发表时间: 2008
• 作者: Eijiro Sumii;Benjamin C.Pierce;Naoki Kobayashi
• 通讯作者: Naoki Kobayashi

A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes

• DOI: 10.1109/lics.2009.29
• 发表时间: 2009-08
• 期刊: 2009 24th Annual IEEE Symposium on Logic In Computer Science
• 作者: N. Kobayashi;C. Ong

Untyped Recursion Schemes and Infinite Intersection Types

无类型递归方案和无限交集类型

• 发表时间: 2010
• 期刊: Proceedings of the 13th International Conference on Foundations of Software Science and Computational Structures (FOSSACS'10) 6014
• 作者: Takeshi Tsukada;Naoki Kobayashi
• 通讯作者: Naoki Kobayashi