Study of Verification of Security of Programs based on Term Rewriting Systems and Tree Automata
| Project/Area Number |
20300010
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
SAKABE Toshiki 名古屋大学, 大学院・情報科学研究科, 教授 (60111829)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
SAKAI Masahiko 名古屋大学, 大学院・情報科学研究科, 教授 (50215597)
|
|---|
| Project Period (FY) |
2008 – 2011
|
| Project Status |
Completed (Fiscal Year 2011)
|
| Budget Amount *help |
¥12,610,000 (Direct Cost: ¥9,700,000、Indirect Cost: ¥2,910,000)
Fiscal Year 2011: ¥2,340,000 (Direct Cost: ¥1,800,000、Indirect Cost: ¥540,000)
Fiscal Year 2010: ¥2,470,000 (Direct Cost: ¥1,900,000、Indirect Cost: ¥570,000)
Fiscal Year 2009: ¥3,250,000 (Direct Cost: ¥2,500,000、Indirect Cost: ¥750,000)
Fiscal Year 2008: ¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000)
|
|---|
| Keywords | 仕様記述 / 仕様検証 / 安全性 / 非干渉性 / 項書き換え系 / 木オートマトン / SMTソルバー / ホオートマトン / モデル検査 / 車載LANプロトコル |
|---|
| Research Abstract |
The purpose of this project is to develop methods for verifying properties of programs by applying techniques of term rewriting and tree automata. The results are methods for verifying automotive LAN protocols and proving program equivalence, and automated generation of loop invariants of imperative programs. In addition, we have obtained several results which are basic to program verification : methods for proving termination of term rewriting systems, efficient SAT solvers for propositional logic and SMT solvers for equational logic.
|
Report
(6 results)
Research Products
(60 results)
