Advancement and Application of Type Theory for Improving Software Safety

• Project/Area Number: 20240001
• Research Category: Grant-in-Aid for Scientific Research (A)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Fundamental theory of informatics
• Research Institution: Tohoku University
• Principal Investigator: KOBAYASHI Naoki Tohoku University, 情報科学研究科, 教授 (00262155)
• Co-Investigator(Kenkyū-buntansha): IGARASHI Atsushi 京都大学, 大学院・情報学研究科, 准教授 (40323456) ; SUMII Eijiro 東北大学, 大学院・情報科学研究科, 准教授 (00333550) ; MATSUDA Kazutaka 東北大学, 大学院・情報科学研究科, 助教 (10583627) ; TERAUCHI Tachio 東北大学, 大学院・情報科学研究科, 助教 (70447150)
• Project Period (FY): 2008 – 2010
• Project Status: Completed (Fiscal Year 2011)
• Budget Amount: ¥49,270,000 (Direct Cost: ¥37,900,000、Indirect Cost: ¥11,370,000); Fiscal Year 2011: ¥10,920,000 (Direct Cost: ¥8,400,000、Indirect Cost: ¥2,520,000); Fiscal Year 2010: ¥13,520,000 (Direct Cost: ¥10,400,000、Indirect Cost: ¥3,120,000); Fiscal Year 2009: ¥10,920,000 (Direct Cost: ¥8,400,000、Indirect Cost: ¥2,520,000); Fiscal Year 2008: ¥13,910,000 (Direct Cost: ¥10,700,000、Indirect Cost: ¥3,210,000)
• Keywords: ソフトウェア検証 / 型システム / 高階モデル検査 / 資源使用法検証 / プログラム解析 / 型理論 / 述語抽象化 / メモリ使用法解析 / モデル検査 / 高階再帰スキーム / 資源使用法解析 / ツリーオートマトン

Research Abstract

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.

Research Products

• [Journal Article] Orderd Types for Stream Processing of Tree-Structured Date (2011)
  • Author(s): Ryosuke Sato, Kohei Suenaga, Naoki Kobayashi
  • Journal Title: Jornal of Information Processing Volume: Vol.52 Pages: 1-14
  • Peer Reviewed
• [Journal Article] A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes (2011)
  • Author(s): Naoki Kobayashi
  • Journal Title: Proceedings of the 14th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2011)
  • Peer Reviewed
• [Journal Article] A hybrid type system for lock-freedom of mobile processes (2010)
  • Author(s): Naoki Kobayashi, Davide Sangiorgi
  • Journal Title: ACM Transactions on Programming Languages and Systems (TOPLAS) Volume: 16 Pages: 49-49
  • Peer Reviewed
• [Journal Article] A logical foundation for environment classifiers (2010)
  • Author(s): Takeshi Tsukada and Atsushi Igarashi
  • Journal Title: Logical Methods in Computer Science Volume: 6巻 Pages: 1-43
  • Peer Reviewed
• [Journal Article] Higher-Order Multi-parameter Tree Transducers and Recursion Schemes for Program Verification (2010)
  • Author(s): Naoki Kobayashi, Naoshi Tabuchi and Hiroshi Unno
  • Journal Title: roceedings of the 37th ACM SIGPLAN-SIGACT Symposium on principles of Programming Languages (POPL 2010) Pages: 495-508
  • Peer Reviewed
• [Journal Article] A hybrid type system for lock-freedom of mobile processes (2010)
  • Author(s): Naoki Kobayashi, Davide Sangiorgi
  • Journal Title: ACM Transactions on Programming Languages and Systems (TOPLAS) Article Number 16 Pages: 49-49
  • Peer Reviewed
• [Journal Article] A logical foundation for environment classifiers (2010)
  • Author(s): Takeshi Tsukada, Atsushi Igarashi
  • Journal Title: Logical Methods in Computer Science 6(4:8) Pages: 1-43
  • Peer Reviewed
• [Journal Article] Higher-Order Multi-parameter Tree Transducers and Recursion Schemes for Program Verification (2010)
  • Author(s): Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno
  • Journal Title: Proceedings of the 37^<th> ACM SIGPLAN-SIGACT Symposium on principles of Programming Languages (POPL 2010) Pages: 495-508
  • Peer Reviewed
• [Journal Article] Verification of Tree-Processing Programs via Higher-Order Model Checking (2010)
  • Author(s): Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi
  • Journal Title: Proceedings of the 8th Asian Symposium on Programming Languages and Systems (APLAS2010), Springer LNCS Pages: 312-327
  • Peer Reviewed
• [Journal Article] ポインタのあるプログラミング言語のための資源使用法解析 (2010)
  • Author(s): 上野慎平, 小林直樹, 海野広志
  • Journal Title: 情報処理学会論文誌:プログラミング Volume: Vol.3 Pages: 27-42
  • NAID: 110007970954
  • Peer Reviewed
• [Journal Article] Environmental Bisimulations for Higher-Order Languages (2010)
  • Author(s): Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii
  • Journal Title: ACM Transactions on Programming Languages and Systems (TOPLAS) Volume: Vol.33
  • Peer Reviewed
• [Journal Article] On Bounding Problems of Quantitative Information Flow (2010)
  • Author(s): Hirotoshi Yasuoka, Tachio Terauchi
  • Journal Title: Proceedings of the 15th European Symposium on Research in Computer Security (ESORICS 2010) Lecture Notes in Computer Science Volume: 6345 Pages: 357-372
  • Peer Reviewed
• [Journal Article] Quantitative Information Flow-Verification Hardness and Possibilities (2010)
  • Author(s): Hirotoshi Yasuoka, Tachio Terauchi
  • Journal Title: Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF 2010), IEEE Computer Society Pages: 15-27
  • Peer Reviewed
• [Journal Article] A logical foundation for environment classifiers (2010)
  • Author(s): Takeshi Tsukada, Atsushi Igarashi
  • Journal Title: Logical Methods in Computer Science Volume: 6(4:8)巻 Pages: 1-43
  • Peer Reviewed
• [Journal Article] Polymorphic Contracts (2010)
  • Author(s): Joao Filipe Belo, Michael Greenberg, Atsushi Igarashi, Benjamin C.Pierce
  • Journal Title: Proceedings of European Symposium on Programming (ESOP2011)
  • Peer Reviewed
• [Journal Article] Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification (2010)
  • Author(s): Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno
  • Journal Title: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'10) Pages: 495-508
  • Peer Reviewed
• [Journal Article] Untyped Recursion Schemes and Infinite Intersection Types (2010)
  • Author(s): Takeshi Tsukada, Naoki Kobayashi
  • Journal Title: Proceedings of the 13th International Conference on Foundations of Software Science and Computational Structures (FOSSACS'10) 6014 Pages: 343-357
  • Peer Reviewed
• [Journal Article] Dependent types from counterexamples (2010)
  • Author(s): Tachio Terauchi
  • Journal Title: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPL'10) 45 Pages: 119-130
  • Peer Reviewed
• [Journal Article] Recursion Schemes for Verification of Higher-Order Programs (2009)
  • Author(s): Naoki Kobayashi, Types and Higher-Order
  • Journal Title: Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on principles of Programming Languages (POPL 2009) Pages: 416-428
  • Peer Reviewed
• [Journal Article] Undecidable Equivalences for Basic Parallel Processes (2009)
  • Author(s): Hans Huttel, Naoki Kobayashi and Takashi Suto
  • Journal Title: Information and Computation Volume: 207(7)巻 Pages: 812-819
  • Peer Reviewed
• [Journal Article] Types and Higher-Order Recursion Schemes for Verification of Higher-Order Programs (2009)
  • Author(s): Naoki Kobayashi
  • Journal Title: Proceedings of the 36^<th> ACM SIGPLAN-SIGACT Symposium on principles of Programming Languages (POPL 2009) Pages: 416-428
  • Peer Reviewed
• [Journal Article] Undecidable Equivalences for Basic Parallel Processes (2009)
  • Author(s): Hans Huttel, Naoki Kobayashi, Takashi suto
  • Journal Title: Information and Computation 207(7)巻 Pages: 812-819
  • Peer Reviewed
• [Journal Article] Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus (2009)
  • Author(s): Naoki Kobayashi, C.-H. Luke Ong
  • Journal Title: Proceedings of the 36th Internatilonal Collogquium on Automata, Languages and Programming(ICALP'09) 5556(2) Pages: 223-234
  • Peer Reviewed
• [Journal Article] Undecidable Equivalences for Basic Parallel Processes (2009)
  • Author(s): Hans Huttel, Naoki Kobayashi, Takashi Suto
  • Journal Title: Information and Computation 207(7) Pages: 812-819
  • Peer Reviewed
• [Journal Article] A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes (2009)
  • Author(s): Naoki Kobayashi, C.-H. Luke Ong
  • Journal Title: Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science(LICS'09) Pages: 179-188
  • Peer Reviewed
• [Journal Article] Model-Checking Higher-Order Functions (2009)
  • Author(s): Naoki Kobayashi
  • Journal Title: Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming(PPDP'09) Pages: 25-36
  • Peer Reviewed
• [Journal Article] Dependent Type Inference with Interpolants (2009)
  • Author(s): Hiroshi Unno, Naoki Kobayashi
  • Journal Title: Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming(PPDP'09) Pages: 277-288
  • Peer Reviewed
• [Journal Article] A Logical Foundation for Environment Classifiers (2009)
  • Author(s): Takeshi Tsukada, Atsushi Igarashi
  • Journal Title: Proceedings of the 9th International Conference on Typed Lambda Calculi and Applications(TLCA'09) Pages: 341-355
  • Peer Reviewed
• [Journal Article] A Complete Characterization of Observational Equivalence in Polymorphic lambda-Calculus with General References (2009)
  • Author(s): Eijiro Sumii
  • Journal Title: Proceedings of the 18th EACSL Annual Conference on Computer Science Logic(CSL'09) 5771 Pages: 455-469
  • Peer Reviewed
• [Journal Article] Polymorphic Fractional Capabilities (2009)
  • Author(s): Hirotoshi Yasuoka, Tachio Terauchi
  • Journal Title: Proceedings of the 16th International Symposium on Static Analysis(SAS'09) 5673 Pages: 36-51
  • Peer Reviewed
• [Journal Article] Types and Higher-Order Recursion Schemes for Verification of Higher-Order Programs (2009)
  • Author(s): Naoki Kobayashi
  • Journal Title: Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPL2009) Pages: 416-428
  • Peer Reviewed
• [Journal Article] Tree Automata for Non-Linear Arithmetic (2008)
  • Author(s): Naoki Kobayashi, Hitoshi Ohsaki
  • Journal Title: Proceedings of the 19th International Conference on Rewriting Techniques and Applications(RTA'08) 5117 Pages: 291-305
  • Peer Reviewed
• [Journal Article] A Hybrid Type System for Lock-Freedom of Mobile Processes (2008)
  • Author(s): Naoki Kobayashi, Davide Sangiorgi
  • Journal Title: Proceedings of the 20th International Conference on Computer Aided Verification(CAV'08) 5123 Pages: 80-93
  • Peer Reviewed
• [Presentation] Higher-order model checking for program verification (2010)
  • Author(s): Naoki Kobayashi
  • Organizer: Workshop on automata and logic for data manipulating programs
  • Place of Presentation: フランスパリ
  • Year and Date: 2010-12-07
• [Presentation] Higher-order model checking for program verification (2010)
  • Author(s): Naoki Kobayashi
  • Organizer: Workshop on automata and logic for data manipulating programs
  • Place of Presentation: フランスパリ,招待講演.
  • Year and Date: 2010-12-07
• [Presentation] Higher-order model checking for program verification (2010)
  • Author(s): Naoki Kobayashi
  • Organizer: Workshop on automata and logic for data manipulating programs
  • Place of Presentation: フランス・パリ
  • Year and Date: 2010-12-07
• [Presentation] Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification (2010)
  • Author(s): Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno
  • Organizer: 日本ソフトウェア科学会第27回特別講演
  • Place of Presentation: 日本・東京
  • Year and Date: 2010-09-13
• [Presentation] Model-Checking Higher-Order Programs (2010)
  • Author(s): Naoki Kobayashi
  • Organizer: Daghstul seminar on Game Semantics and Program Verification
  • Place of Presentation: ドイツ・ダーグストゥール
  • Year and Date: 2010-06-21
• [Presentation] Types and Recursion Schemes for Higher-Order Program Verification (2010)
  • Author(s): Naoki Kobayashi
  • Organizer: Workshop on Higher-Order Recursion Schemes and Pushdown Automata
  • Place of Presentation: フランスパリ
  • Year and Date: 2010-03-11
• [Presentation] Types and Recursion Schemes for Higher-Order Program Verification (2010)
  • Author(s): Naoki Kobayashi
  • Organizer: Workshop on Higher-Order Recursion Schemes and Pushdown Automata
  • Place of Presentation: フランスパリ,招待講演.
  • Year and Date: 2010-03-11
• [Presentation] Types and Recursion Schemes for Higher-Order Program Verification (2009)
  • Author(s): Naoki Kobayashi
  • Organizer: the 7th Asian Symposium on Programming Languages and Systems (APLAS 2009)
  • Place of Presentation: 韓国ソウル
  • Year and Date: 2009-12-16
• [Presentation] Higher-Order Program Verification and Language-Based Security (2009)
  • Author(s): Naoki Kobayashi
  • Organizer: the 13th Annual Asian Computing Science Conference (ASIAN 2009)
  • Place of Presentation: 韓国ソウル
  • Year and Date: 2009-12-16
• [Presentation] Types and Recursion Schemes for Higher-Order Program Verification (2009)
  • Author(s): Naoki Kobayashi
  • Organizer: the 7th Asian Symposium on Programming Languages and Systems (APLAS 2009)
  • Place of Presentation: 韓国ソウル,招待講演.
  • Year and Date: 2009-12-16
• [Presentation] Higher-Order Program Verification and Language-Based Security (2009)
  • Author(s): Naoki Kobayashi
  • Organizer: the 13th Annual Asian Computing Science Conference (ASIAN 2009)
  • Place of Presentation: 韓国ソウル,招待講演.
  • Year and Date: 2009-12-16
• [Presentation] Higher-Order Program Verification and Language-Based Security (2009)
  • Author(s): Naoki Kobayashi
  • Organizer: 13th Annual Asian Computing Science Conference (ASIAN'09)
  • Place of Presentation: 韓国・ソウル
  • Year and Date: 2009-12-16
• [Presentation] Types and Recursion Schemes for Higher-Order Program Verification (2009)
  • Author(s): Naoki Kobayashi
  • Organizer: 7th Asian Symposium on Programming Languages and Systems (APLAS'09)
  • Place of Presentation: 韓国・ソウル
  • Year and Date: 2009-12-16
• [Presentation] Substructural Type Systems for Program Analysis (2008)
  • Author(s): Naoki Kobayashi
  • Organizer: The 9th International Symposium on Functional and Logic Programming (FLOPS 2008)
  • Place of Presentation: 三重県伊勢市
  • Year and Date: 2008-04-16
• [Presentation] Substructural Type Systems for Program Analysis (2008)
  • Author(s): Naoki Kobayashi
  • Organizer: The 9th International Symposium on Functional and Logic Programming (FLOPS 2008)
  • Place of Presentation: 三重県伊勢市,招待講演.
  • Year and Date: 2008-04-16
• [Presentation] Substructural Type Systems for Program Analysis (2008)
  • Author(s): Naoki Kobayashi
  • Organizer: The 9th International Symposium on Functional and Logic Programming(FLOPS'08)
  • Place of Presentation: 三重県伊勢市
  • Year and Date: 2008-04-16
• [Remarks]
  • URL: http://www.kb.ecei.tohoku.ac.jp/