形式検証 - pogi-log

形式検証

形式検証(けいしきけんしょう、formal verification)

形式的検証とWikipediaはなってるけど、ここは形式検証にしておく

ソフトウェアにバグがないことを検証して、保証する

述内容に論理的な矛盾など何らかの観点からの不整合があるか否かを確認するVerification

ref: 『ソフトウェア工学の道具としての形式手法 Formal Methods as Software Engineering Tools』

検証(Verification)と妥当性検証(Validation)

形式的検証の手法

モデル検査

線形時相論理 (LTL)

計算木論理 (CTL)

論理的推論

定理証明ソフトウェア

etc

数理モデル

有限オートマトン

ペトリネット

プロセス計算

確認用

Q. 形式的検証

参考

形式的検証 - Wikipedia

関連

Homotopy Type Theory(HoTT)