3J-02
SMTソルバを用いた仕様に関する定理の証明とソフトウェア開発への応用
○小松秀生，岡本圭史（仙台高専）
昨今,要求されるソフトウェアが年々複雑化しており,高信頼性を保証するソフトウェア開発手法が強く求められている.そのような課題を解決する手段として,形式手法に注目が集まっているが,数学的知識が必要になるため導入が容易でない.その問題に対して、論文Theory of Programsで紹介されている枠組みを利用することで,形式的な仕様検証の導入を容易にできると我々は考えている.しかし,その論文で紹介されている定理の証明は人手で行われており,間違いが混入しがちである.そこで本研究では,Theory of Programsの仕様に関する定理を,SMTソルバの一つであるZ3を用いて検証し,形式的な証明を与える.さらに,それらの定理を用いた仕様検証の事例を示す.
footer 著作権について 倫理綱領 プライバシーポリシー セキュリティ 情報処理学会