ソフトウェアの安全性向上のための型理論の深化と応用

2010 年度 自己評価報告書

• 研究課題/領域番号: 20240001
• 研究種目: 基盤研究(A)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: 情報学基礎
• 研究機関: 東北大学
• 研究代表者: 小林 直樹 東北大学, 大学院・情報科学研究科, 教授 (00262155)
• 研究期間 (年度): 2008 – 2010
• キーワード: ソフトウェア検証 / 型システム / 高階モデル検査 / 資源使用法検証 / プログラム解析

研究概要

交通システムや金融システム・原子力発電など重要な社会基盤の多くがコンピュータによって制御されている今日の高度情報化社会においては,ソフトウェアの信頼性向上が極めて重要かつ緊急の課題である.本研究では型システムに基づくソフトウェア検証の理論をさらに発展させ,研究代表者らがこれまでに取り組んできた並行プログラムの通信や同期の整合性,計算資源へのアクセス順序,セキュリティプロトコルなどの検証のための型理論を実用レベルにまで引き上げることを目標とする.また,そのような実用化に向けた研究を通じて,(1)ポインタや例外,割り込みなどの現実のプログラムに存在する複雑な言語機構を扱うための拡張,(2)検証精度と速度の向上,(3)モデル検査や定理証明など他の検証手法との融合,などの技術的課題 に取り組む

研究成果

• [雑誌論文] A hybrid type system for lock-freedom of mobile processes (2010)
  • 著者名/発表者名: Naoki Kobayashi, Davide Sangiorgi
  • 雑誌名: ACM Transactions on Programming Languages and Systems (TOPLAS) Article Number 16 ページ: 49
  • 査読あり
• [雑誌論文] A logical foundation for environment classifiers (2010)
  • 著者名/発表者名: Takeshi Tsukada, Atsushi Igarashi
  • 雑誌名: Logical Methods in Computer Science 6(4:8) ページ: 1-43
  • 査読あり
• [雑誌論文] Higher-Order Multi-parameter Tree Transducers and Recursion Schemes for Program Verification (2010)
  • 著者名/発表者名: Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno
  • 雑誌名: Proceedings of the 37^<th> ACM SIGPLAN-SIGACT Symposium on principles of Programming Languages (POPL 2010) ページ: 495-508
  • 査読あり
• [雑誌論文] Types and Higher-Order Recursion Schemes for Verification of Higher-Order Programs (2009)
  • 著者名/発表者名: Naoki Kobayashi
  • 雑誌名: Proceedings of the 36^<th> ACM SIGPLAN-SIGACT Symposium on principles of Programming Languages (POPL 2009) ページ: 416-428
  • 査読あり
• [雑誌論文] Undecidable Equivalences for Basic Parallel Processes (2009)
  • 著者名/発表者名: Hans Huttel, Naoki Kobayashi, Takashi suto
  • 雑誌名: Information and Computation 207(7)巻 ページ: 812-819
  • 査読あり
• [学会発表] Higher-order model checking for program verification (2010)
  • 著者名/発表者名: Naoki Kobayashi
  • 学会等名: Workshop on automata and logic for data manipulating programs
  • 発表場所: フランスパリ,招待講演.
  • 年月日: 2010-12-07
• [学会発表] Types and Recursion Schemes for Higher-Order Program Verification (2010)
  • 著者名/発表者名: Naoki Kobayashi
  • 学会等名: Workshop on Higher-Order Recursion Schemes and Pushdown Automata
  • 発表場所: フランスパリ,招待講演.
  • 年月日: 2010-03-11
• [学会発表] Types and Recursion Schemes for Higher-Order Program Verification (2009)
  • 著者名/発表者名: Naoki Kobayashi
  • 学会等名: the 7th Asian Symposium on Programming Languages and Systems (APLAS 2009)
  • 発表場所: 韓国ソウル,招待講演.
  • 年月日: 2009-12-16
• [学会発表] Higher-Order Program Verification and Language-Based Security (2009)
  • 著者名/発表者名: Naoki Kobayashi
  • 学会等名: the 13th Annual Asian Computing Science Conference (ASIAN 2009)
  • 発表場所: 韓国ソウル,招待講演.
  • 年月日: 2009-12-16
• [学会発表] Substructural Type Systems for Program Analysis (2008)
  • 著者名/発表者名: Naoki Kobayashi
  • 学会等名: The 9th International Symposium on Functional and Logic Programming (FLOPS 2008)
  • 発表場所: 三重県伊勢市,招待講演.
  • 年月日: 2008-04-16