@inproceedings{oai:ipsj.ixsq.nii.ac.jp:00107876,
 author = {山田一宏 and 森口草介 and 渡部卓雄 and 西崎真也},
 book = {第73回全国大会講演論文集},
 issue = {1},
 month = {Mar},
 note = {我々は，Morrisの2分木走査アルゴリズムのCによる実装を対象として，証明支援系を用いた正当性の検証を試みた．本論文はその手法と結果に関する報告である．Morrisのアルゴリズムは，ポインタの書き換えを行うことで再帰やスタックを用いずに2分木走査を行う方法のひとつである．また他のポインタ反転法と異なり節点に印を付けるためのビットを設ける必要もないのが特徴である．我々は，入力および走査結果についての仕様を事前・事後条件として与え，C用の検証支援ツールであるCaduceusによって検証条件を生成した．ループ不変条件は必要に応じて適宜与えた．生成された検証条件を自動検証ツールSimplifyおよび証明支援系Coqを用いて証明した．},
 pages = {505--506},
 publisher = {情報処理学会},
 title = {証明支援系を用いたMorrisの2分木走査アルゴリズムの実装の検証},
 volume = {2011},
 year = {2011}
}