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