Fundamental research on software verification based on algebraic method
Grant-in-Aid for Scientific Research (C)
|Allocation Type||Single-year Grants|
|Research Institution||Nagoya University(1997)|
Japan Advanced Institute of Science and Technology(1995-1996)
SAKAI Masahiko Dept.of Engineering, Nagoya Univ., Assoc.Professor, 工学研究科, 助教授 (50215597)
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
Completed(Fiscal Year 1997)
|Budget Amount *help
¥2,300,000 (Direct Cost : ¥2,300,000)
Fiscal Year 1997 : ¥800,000 (Direct Cost : ¥800,000)
Fiscal Year 1996 : ¥700,000 (Direct Cost : ¥700,000)
Fiscal Year 1995 : ¥800,000 (Direct Cost : ¥800,000)
|Keywords||term rewriting system / confluence / termination / E-unification / completion|
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.
Research Output (22results)