| 研究概要 |
SMTの実装のひとつであるcvc3を利用し、最弱事前条件計算を実装した。現状他のSMTでは,充足可能であるとき、具体的な1つのモデルを得ることができるのみで、全ての充足可能な場合を得るためのインタフェースが提供されていない。したがって、ソースコードが公開され利用法の自由度が高いcvc3を利用した。
最弱事前条件計算を用いて、不動点帰納法と補題発見器、述語間の導出関係をチェックする機能をSMTを利用して実装した。補題発見器では、補題候補として元となる述語の部分論理式から自動的に生成する。より有用な候補から順に調ベチェックすることで、補題発見に成功したときに残りの多くの候補を検査しなくとも良い様にした。
こうして、補題発見器を備えた最小構成の不変性自動検証器を実装したものの、単にSMTを使用して実装しただけでは、プロセス間通信を多用したこれまでの実装と比べても、実行速度ではほとんど改善が見られなかった。そこで、・最弱事前条件を計算する述語に応じて、不要な述語を省き、述語数を抑えた。
・述語間の導出関係の検査は、SMTに計算させると非常に時間がかかるため、2段チェックにし、多くの場合SMTを使用しなくともチェックできるようにした。
・補題候補チェックは、アルゴリズム上重複が発生しやすいので、結果をキャッシュするようにした。
・その他、述語を簡単化するようにし、各処理の効率化を図った。
以上により、全体として3倍～数十倍程度の高速化を実現した。
分散化については、設計から考慮に入れてはいるが、シングルスレッド性能の改善のために時間を費やしたため、現状は分散化できていない。30コントロールロケーション程度の規模の例題で、20分ほどで証明できた。より大規模になれば、分散化は必須であるので、今後も継続して開発し、分散化したい。
|
