Fundamental research on software verification based on algebraic method

基于代数方法的软件验证基础研究

• 批准号: 07680350
• 负责人: SAKAI Masahiko
• 金额: $ 1.47万
• 依托单位: Nagoya University (1997)Japan Advanced Institute of Science and Technology (1995-1996)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 1995
• 资助国家: 日本
• 起止时间: 1995 至 1997
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-07680350/
• 关键词: 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.

本研究的目的是建立方程逻辑的验证方法，并通过将软件转化为方程来应用软件验证。得到以下结果：(1)将终止方程视为序数项重写规则，将非终止方程视为双手都有项集的重写规则，定义了术语集重写系统。(2)术语集重写系统如果相应的 E 重写正在终止，则终止。(3) 如果所有关键对都是可连接的，则终止和左线性术语集重写系统是汇合的。(4) 术语集完成的推理规则定义了重写系统。(5)通过构建实验系统，研究了术语集重写系统的有效实现。(6)讨论了重写系统关于结合律和交换律商的终止性质。(7)提供优先术语重写系统。

项目成果

Takashi Nagaya: "Index Reduction of Overlapping Strong Sequential Systems" Tech. Rep,of IEICE. COMP96・32. 39-48 (1996)

Takashi Nagaya：“重叠强顺序系统的索引减少”技术，IEICE COMP96・32（1996）。

Masahiko Sakai: "Semantics and Strong Sequentiality of Prioority Term Rewriting Systems" Proc. on Rewriting Techniques and AppricatIon,LNCS. 1103. 377-391 (1996)

Masahiko Sakai：“优先术语重写系统的语义和强顺序性”Proc。

Y.Takahashi, M.Sakai, Y.Toyama: "On the confluence property of conditional term rewriting systems" Transactions of IEICE. J79-D-I (in Japanese). 897-902 (1996)

Y.Takahashi、M.Sakai、Y.Toyama：“论条件项重写系统的汇合性”，IEICE 汇刊。

草刈圭一朗: "非線形項書換え系の合流性について" 電子情報通信学会 技術報告. COMP95‐86. 123-129 (1996)

Keiichiro Kusakari：“非线性术语重写系统的汇合”IEICE COMP95-86 (1996)。

H.Kasuya, M.Sakai, S.Yamamoto, K.Agusa: "Term Set Rewriting Systems and their Confluent Property" Transactions of IEICE. J80-D-I (in Japanese). 325-334 (1997)

H.Kasuya、M.Sakai、S.Yamamoto、K.Agusa：IEICE 的“术语集重写系统及其融合属性”交易。