|
本研究では、不動点帰納法による検証能力の向上、適用可能規模の向上のため、テストに基づく発見的手法により帰納法の仮定を求め(補題発見)、従来手法では自動検証できなかった問題に対しても、自動的な検証を行えるようにすることを目的とする。SMTソルバとしてCVC3を利用して最弱事前条件計算を実装し、補題発見機能と不動点帰納法による不変性自動検証器を実装した。SMTを用いたことや補題の発見、各種手続きの効率化を図ることで、証明力の向上と数十倍程度の高速化を実現し、より規模の大きな問題であっても、自動で証明できるようになった。
|
