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 *help |
¥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.
|
Report
(6 results)
Research Products
(13 results)
