Home >

news Help

Publication Information


Title
Japanese:証明支援系を用いたMorrisの二分木走査アルゴリズムの検証 
English:Verifying C Source Code using Proof Assistant Tools: A Case Study with Morris' Tree Traversal Algorithm 
Author
Japanese: 山田一宏, 渡部卓雄, 森口草介, 西崎真也.  
English: Kazuhiro Yamada, Takuo Watanabe, Sosuke Moriguchi, Shin-ya Nishizaki.  
Language Japanese 
Journal/Book name
Japanese:情報処理学会研究報告ソフトウェア工学 
English:IPSJ SIG Notes 
Volume, Number, Page Vol. SE-171    No. 26    pp. 1-4
Published date Mar. 7, 2011 
Publisher
Japanese: 
English: 
Conference name
Japanese:情報処理学会ソフトウェア工学研究会 
English:IPSJ SIGSE 
Conference site
Japanese:東京都千代田区 
English: 
Official URL http://ci.nii.ac.jp/naid/110008583134
 
Abstract 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.

©2007 Tokyo Institute of Technology All rights reserved.