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程序和加密协议构建了验证工具。作为后一项研究，我们已经显示了高阶模型检查对程序验证的新颖应用，并构建了世界上第一个高阶模型检查器。

项目成果

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

Polymorphic Contracts

多态合约

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

Types and Higher-Order Recursion Schemes for Verification of Higher-Order Programs

• DOI: 10.1145/1594834.1480933
• 发表时间: 2009-01-01
• 期刊: ACM SIGPLAN NOTICES
• 作者: Kobayashi, Naoki

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