• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Fundamental research on software verification based on algebraic method

Research Project

Project/Area Number 07680350
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeSingle-year Grants
Section一般
Research Field 計算機科学
Research InstitutionNagoya 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
Project Status 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)
Keywordsterm 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.

Report

(4 results)
  • 1997 Annual Research Report   Final Research Report Summary
  • 1996 Annual Research Report
  • 1995 Annual Research Report
  • Research Products

    (22 results)

All Other

All Publications (22 results)

  • [Publications] 高橋、酒井、外山: "条件付き項書換え系の合流性について" 電子情報通信学会論文誌. J79-D-I. 897-902 (1996)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] 粕谷, 酒井, 山本, 阿草: "項集合書換え系とその合流性" 電子情報通信学会論文誌. J80-D-I. 325-334 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] M.Sakai: "Left-Incompatible Term Rewriting Systems and Functional Strategy" IEICE Trans. on Information and System. E80-D. 1176-1182 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] M.Sakai, Y.Toyama: "Semantics and Strong Sequentiality of Priority Term Rewriting Systems" Theoretical Computer Science. (to appear). (1998)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] 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)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] 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)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] M.Sakai: "Left-Incompatible Term Rewriting Systems and Functional Strategy" IEICE Trans.on Information and System. E80-D. 1176-1182 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] M.Sakai, Y.Toyama: "Semantics and Strong Sequentiality of Priority Term Rewriting Systems" Theoretical Computer Science. (to appear). (1998)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] 粕谷,酒井,山本,阿草: "項集合書換え系とその合流性" 電子情報通信学会論文誌. J80-D-I. 325-334 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] M. Sakai: "Left-Incompatible Term Rewriting Systems and Functional Strategy" IEICE Trans. on Information and System. E80-D. 1176-1182 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] M.Sakai, Y.Toyama: "Semantics and Strong Sequentiality of Priority Term Rewriting Systems" Theoretical Computer Science. (to appear). (1998)

    • Related Report
      1997 Annual Research Report
  • [Publications] 高橋宜孝: "条件付き項書換え系の合流性について" 電子情報通信学会論文誌. J79-D-l011. 897-902 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 粕谷英人: "項集合書換え系とその合流性" 電子情報通信学会論文誌. 掲載予定.

    • Related Report
      1996 Annual Research Report
  • [Publications] Masahiko Sakai: "Semantics and Strong Sequentiality of Prioority Term Rewriting Systems" Proc. on Rewriting Techniques and AppricatIon,LNCS. 1103. 377-391 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] Keiichiro Kusakari: "Church-Rosser Property of Finite Ranked Terms of Non-linear Term Rewriting Systems" LAシンポジウム論文集. 160-165 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] Takashi Nagaya: "Index Reduction of Overlapping Strong Sequential Systems" Tech. Rep,of IEICE. COMP96・32. 39-48 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] Munehiro Iwami: "An Improved Recursive Decomposition Ordering for Higher-order Rewrite Systems" Tech Rep. of IEICF. COMP96・73. 17-24 (1997)

    • Related Report
      1996 Annual Research Report
  • [Publications] 酒井正彦: "The Functional Strategy-The Extended Left‐incompatible System" 電子情報通信学会 技術報告. SS95‐17. 55-62 (1995)

    • Related Report
      1995 Annual Research Report
  • [Publications] 酒井正彦: "The Semantics of Priority Term Rewriting Systems and their Strong sequentiality" 電子情報通信学会 技術報告. SS95‐40. 31-38 (1996)

    • Related Report
      1995 Annual Research Report
  • [Publications] 岩見宗弘: "高階項書換え系の停止性について" 電子情報通信学会 技術報告. COMP95‐85. 113-121 (1996)

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

    • Related Report
      1995 Annual Research Report
  • [Publications] 中野賢司: "項書換え系のAC停止性について" 電子情報通信学会 技術報告. COMP(発表予定). (1996)

    • Related Report
      1995 Annual Research Report

URL: 

Published: 1995-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi