2026-03-14T17:39:25Z https://ipsj.ixsq.nii.ac.jp/oai

oai:ipsj.ixsq.nii.ac.jp:00074122 2025-01-21T21:41:31Z 1164:1384:6349:6417

証明支援系を用いたMorrisの二分木走査アルゴリズムの検証 Verifying C Source Code using Proof Assistant Tools ―A Case Study with Morris’ Tree Traversal Algorithm― 山田, 一宏 渡部, 卓雄 森口, 草介 西崎, 真也 Kazuhiro, Yamada Takuo, Watanabe Sosuke, Moriguchi Shin-ya, Nishizaki 検証・検査 我々はMorrisのアルゴリズムのCによる実装の検証を試みた．このアルゴリズムは再帰やスタックを用いずに二分木の走査を行うものであり，節点内部に余分なタグも不要であるという特徴がある．本研究はポインタ操作を伴うCプログラムへの検証支援ツール適用のケーススタディであり，今回は検証支援系CaduceusおよびWhy，自動証明系Simplifyおよび対話的証明支援系Coqを使用した．本稿では，これらによる検証手法とその結果の概要を述べる． We proved the partial correctness of a C implementation of Morris's tree traversal algorithm. The algorithm is known as a recursion-free, stack-free and tag-free binary tree traversal. This work is intended to be a case study of verifying C programs with pointer manipulation using existing verification tools such as Caduceus, Why, Simplify and Coq. In this report, we describe the outline of the verification methodology and results. 情報処理学会 2011-03-07 jpn technical report https://ipsj.ixsq.nii.ac.jp/records/74122 AN10112981 研究報告ソフトウェア工学（SE） 2011-SE-171 26 1 4 https://ipsj.ixsq.nii.ac.jp/record/74122/files/IPSJ-SE11171026.pdf application/pdf 265.5 kB 2013-03-07