@article{oai:nagoya.repo.nii.ac.jp:00019054,
 author = {古市, 祐樹 and 西田, 直樹 and 酒井, 正彦 and 草刈, 圭一朗 and 坂部, 俊樹 and Furuichi, Yuki and Nishida, Naoki and Sakai, Masahiko and Kusakari, Keiichirou and Sakabe, Toshiki},
 issue = {2},
 journal = {情報処理学会論文誌, プログラミング},
 month = {Sep},
 note = {手続き型プログラムの検証手法として，モデル検査やホーア論理に基づく検証手法が代表的である．一方，項書換えの分野では帰納的定理の証明手法として潜在帰納法や書換え帰納法などが広く研究されている．本論文では，帰納的定理の証明法を利用して手続き型プログラムの等価性の検証を試みる．具体的には，自然数上のwhile言語で定義された手続き型関数からプレスブルガー文を規則の制約として持つことが許された制約付き項書換え系への変換を与え，その変換により手続き型プログラムの等価性を書換え系の関数の等価性に帰着させ，潜在帰納法を用いて等価性検証を試みる．この手法を実現するために，合流性を保証するための危険対定理および完備化手続きを制約付き書換えに対応するように拡張する．, In the field of procedural programming, several verification methods based on model checking or Hoare logic have been proposed. On the other hand, in the field of term rewriting, implicit induction and rewriting induction have been widely studied as methods for proving inductive theorems. In this paper, we try to take advantages of methods for proving inductive theorems in verifying procedural functions written in a "while" language with natural number type. More precisely, we propose a transformation from procedural programs to constrained term rewriting systems whose constraints are in Presburger arithmetic, and show that the transformation reduces the equivalence of procedural programs to that of functions in rewrite systems. By verifying the equivalence between rewrite systems, we verify the equivalence between the corresponding procedural functions. To establish this approach, we extend Critical Pair Theorem and the basic completion procedure for constrained systems.},
 pages = {100--121},
 title = {制約付き項書換え系の潜在帰納法を利用した手続き型プログラム検証の試み},
 volume = {1},
 year = {2008}
}