Formal Verification of Higher-Order Open Systems

• Project/Area Number: 22300005
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: Tohoku University
• Principal Investigator: SUMII Eijiro 東北大学, 情報科学研究科, 教授 (00333550)
• Co-Investigator(Kenkyū-buntansha): TERAUCHI Tachio 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (70447150)
• Project Period (FY): 2010-04-01 – 2015-03-31
• Project Status: Completed (Fiscal Year 2014)
• Budget Amount: ¥14,690,000 (Direct Cost: ¥11,300,000、Indirect Cost: ¥3,390,000); Fiscal Year 2014: ¥2,600,000 (Direct Cost: ¥2,000,000、Indirect Cost: ¥600,000); Fiscal Year 2013: ¥2,860,000 (Direct Cost: ¥2,200,000、Indirect Cost: ¥660,000); Fiscal Year 2012: ¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000); Fiscal Year 2011: ¥2,860,000 (Direct Cost: ¥2,200,000、Indirect Cost: ¥660,000); Fiscal Year 2010: ¥3,250,000 (Direct Cost: ¥2,500,000、Indirect Cost: ¥750,000)
• Keywords: 環境双模倣 / 並行・分散プロセス計算モデル / プログラム理論 / 形式手法 / 理論計算機科学 / 計算モデル / 分散プロセス計算 / 高階プログラム等価性証明 / 並行・分散プロセス計算 / プログラム意味論 / プロセス計算 / 並行分散システム / 形式的手法

Outline of Final Research Achievements

We developed the first sound and complete theory for proving behavioral equivalence ("makes the same actions" when observed externally) in higher-order (processes themselves can be communicated), concurrent and distributed ("has the notion of locations") computation model (process calculus), and published the results in refereed venues such as LICS 2012, a top conference on theoretical computer science.

Research Products

• [Journal Article] A Simple and Practical Linear Algebra Library with Static Size Checking (2014)
  • Author(s): Akinori Abe, Eijiro Sumii
  • Journal Title: Proceedings of The OCaml Users and Developers Workshop Volume: - Pages: 1-3
  • Peer Reviewed / Acknowledgement Compliant
• [Journal Article] A Multi-Role Translation of Protocol Narration into the Spi-Calculus with Correspondence Assertions (2013)
  • Author(s): Eijiro Sumii and Yuji Sato
  • Journal Title: FCS'13: Workshop on Foundations of Computer Security (Informal Proceedings) Volume: - Pages: 68-82
  • Peer Reviewed
• [Journal Article] A Higher-Order Distributed Calculus with Name Creation (2012)
  • Author(s): Adrien Pierard, Eijiro Sumii
  • Journal Title: Proceedings of Twenty-Seventh Annual ACM/IEEE Symposium on Logic in Computer Science Volume: 27 Pages: 531-540
  • DOI: 10.1109/lics.2012.63
  • Peer Reviewed
• [Journal Article] From Applicative to Environmental Bisimulation (2011)
  • Author(s): Vasileios Koutavas, Paul Blain Levy, Eijiro Sumii
  • Journal Title: Electronic Notes in Theoretical Computer Science Volume: 276 Pages: 215-235
  • DOI: 10.1016/j.entcs.2011.09.023
  • Peer Reviewed
• [Journal Article] Sound Bisimulations for Higher-Order Distributed Process Calculus (2011)
  • Author(s): Adrien Pierard, Eijiro Sumii
  • Journal Title: Lecture Notes in Computer Science Volume: 6604 Pages: 123-137
  • Peer Reviewed
• [Journal Article] Environmental bisimulations for higher-order language (2011)
  • Author(s): Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii
  • Journal Title: ACM Transactions on Programming Language Systems Volume: 33(1)
  • Peer Reviewed
• [Journal Article] A bisimulation-like proof method for contextual properties in untyped lambda-calculus with references and deallocation (2010)
  • Author(s): Eijiro Sumii
  • Journal Title: Theoretical Computer Science Volume: 411(51-52) Pages: 4358-4378
  • Peer Reviewed
• [Presentation] A Simple and Practical Linear Algebra Library with Static Size Checking (2014)
  • Author(s): Eijiro Sumii
  • Organizer: ACM SIGPLAN ML Family Workshop
  • Place of Presentation: Gothenburg, Sweden
  • Year and Date: 2014-09-04
• [Presentation] Sound Bisimulations for Higher-Order Distributed Process Calculus (2011)
  • Author(s): Adrien Pierard, Eijiro Sumii
  • Organizer: 14th International Conference on Foundations of Software Science and Computation Structures
  • Place of Presentation: ドイツ・ザールブリュッケン
  • Year and Date: 2011-03-28
• [Presentation] A Multi-Role Translation of Protocol Narration into the Spi-Calculus with Correspondence Assertions
  • Author(s): Eijiro Sumii
  • Organizer: FCS'13: Workshop on Foundations of Computer Security
  • Place of Presentation: Tulane University, New Orleans, USA
• [Presentation] Environmental Bisimulation and Its Open Problems
  • Author(s): Eijiro Sumii
  • Organizer: IFIP Working Group 2.8
  • Place of Presentation: Aussois, France
• [Presentation] A Higher-Order Distributed Calculus with Name Creation
  • Author(s): Adrien Pierard, Eijiro Sumii
  • Organizer: Twenty-Seventh Annual ACM/IEEE Symposium on Logic in Computer Science
  • Place of Presentation: Dubrovnik, Croatia
• [Presentation] From Applicative to Environmental Bisimulation
  • Author(s): Vasileios Koutavas, Paul Blain Levy, Eijiro Sumii
  • Organizer: Mathematical Foundations of Programming Semantics
  • Place of Presentation: Carnegie Mellon University, Pittsburgh, PA, USA