Formal Verification of Higher-Order Open Systems

2014 Fiscal Year Final Research Report

• 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
• 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.

Free Research Field

プログラミング言語理論