Research on automated program verification based on confluence
| Project/Area Number |
25330004
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Theory of informatics
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
AOTO TAKAHITO 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Project Status |
Completed (Fiscal Year 2015)
|
| Budget Amount *help |
¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000)
Fiscal Year 2015: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2014: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2013: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
|
|---|
| Keywords | 項書き換えシステム / 合流性 / 定理自動証明 / 自動検証 |
|---|
| Outline of Final Research Achievements |
The theory of term rewriting systems is widely used in the fields of automated theorem provings and computation models. Although several automated confluence provers of term rewriting systems have been developed recently, little work is reported on applications of them. This research aims to develop automated program verification methods based on automated confluence provers for term rewriting systems. Concrete results include confluence proving based on persistency and type information, automated inductive theorem proving based on program transformations, sufficient criteria for confluent nominal rewriting systems, a sufficient condition for termination of the tree automata completion, automated ground confluence proving, abstract reduction systems on ordered monoid.
|
Report
(4 results)
Research Products
(12 results)
