1997 Fiscal Year Final Research Report Summary
Fundamental research on software verification based on algebraic method
| Project/Area Number |
07680350
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Nagoya University (1997)
Japan Advanced Institute of Science and Technology (1995-1996) |
|---|
Principal Investigator |
SAKAI Masahiko Dept.of Engineering, Nagoya Univ., Assoc.Professor, 工学研究科, 助教授 (50215597)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
TOYAMA Yoshihito Nagoya University, School of Information Science, JAIST,Professor, 情報科学研究科, 教授 (00251968)
YAMAMOTO Shinichiro Dept.of Engineering, Nagoya Univ., Lecturer, 工学研究科, 講師 (40240098)
|
|---|
| Project Period (FY) |
1995 – 1997
|
| Keywords | term rewriting system / confluence / termination / E-unification / completion |
|---|
| Research Abstract |
This research is toward establishing verification method in equational logic and applying it software verification by transforming software to equations. The following results were obtained ;
(1) The term set rewriting systems are defined by considering terminating equations as ordinal term rewriting rules and non-terminating equations as rewriting rules having sets of terms in both-hand sides.
(2) term set rewriting systems is terminating if the corresponding E-rewriting is terminating.
(3) Terminating and left-linear term set rewriting systems are confluent, if all critical pairs are joinable.
(4) The inference rules for completion on term set rewriting systems are defined.
(5) The efficient implementation of term set rewriting systems are investigated by constructing an experimental system.
(6) The terminating property of rewriting systems on quotients of associative and commutative laws are discussed.
(7) The new semantics of priority term rewriting system was offered.
|
