書換え技術に基づくソフトウエア解析

点击翻译按钮获取中文摘要

停止性を保証する問題は計算機科学の多くの分野で生じる。様々なプログラミング言語においてプログラムが停止することを証明するために、多くの研究がなされてきた。ソフトウェア解析のテクニックであるプログラムの特殊化,部分評価,プログラム変換は、いずれも基盤技術として停止性が必須である。またセーフティクリティカルなシステムでは、正しい動作を保証する必要があるが、このような問題の多くは項書換え系の停止性問題へと帰着させることが可能である。項書換え系の停止性証明の自動化は、従来、単純化順序をベースにしたテクニックを用いていたが、この数年間においては、単純化順序の持つ限界を打破する自動化手法の研究が盛んに行われるようになった。ArtsとGieslの依存対法は、現在注目されている新手法の1つである。依存対法に基づく停止性証明ツールの実現する際には、(1)依存グラフの近似,(2)循環解析,(3)引数フィルタリングの3つの困難がある。最初の2つにより、停止性を証明するために解かなければならない順序制約の集合(連立不等式の一種)の数とサイズが決まる。3つ目により、順序制約の集合を解く際の探索空間のサイズが決まる。これらのサイズと停止性証明の計算コストは比例するが、私たちは新たなアルゴリズムを開発し、そのサイズを劇的に削減することに成功した。このアルゴリズムを停止性自動証明ツールTsukuba Termination Tool上で実装し、数多くの実験を行った。その実験データによりアルゴリズムの有効性が確認された。