Home >

news ヘルプ

論文・著書情報


タイトル
和文:証明支援系を用いた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.  
言語 Japanese 
掲載誌/書名
和文:情報処理学会研究報告ソフトウェア工学 
英文:IPSJ SIG Notes 
巻, 号, ページ Vol. SE-171    No. 26    pp. 1-4
出版年月 2011年3月7日 
出版者
和文: 
英文: 
会議名称
和文:情報処理学会ソフトウェア工学研究会 
英文:IPSJ SIGSE 
開催地
和文:東京都千代田区 
英文: 
公式リンク http://ci.nii.ac.jp/naid/110008583134
 
アブストラクト 我々はMorrisのアルゴリズムのCによる実装の検証を試みた．このアルゴリズムは再帰やスタックを用いずに二分木の走査を行うものであり，節点内部に余分なタグも不要であるという特徴がある．本研究はポインタ操作を伴うCプログラムへの検証支援ツール適用のケーススタディであり，今回は検証支援系CaduceusおよびWhy，自動証明系Simplifyおよび対話的証明支援系Coqを使用した．本稿では，これらによる検証手法とその結果の概要を述べる．

©2007 Institute of Science Tokyo All rights reserved.