2011 Fiscal Year Final Research Report
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
|
| Keywords | 仕様記述 / 仕様検証 |
|---|
| 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.
|
