形式検証
形式検証(けいしきけんしょう、formal verification)
形式的検証とWikipediaはなってるけど、ここは形式検証にしておく
ソフトウェアにバグがないことを検証して、保証する
述内容に論理的な矛盾など何らかの観点からの不整合があるか否かを確認するVerification
ref:
『ソフトウェア工学の道具としての形式手法 Formal Methods as Software Engineering Tools』
V&V
検証(
Verification
)と妥当性検証(
Validation
)
形式的検証の手法
モデル検査
時相論理
線形時相論理 (LTL)
計算木論理 (CTL)
論理的推論
定理証明ソフトウェア
Coq
Isabelle
HOL
Lean
etc
数理モデル
有限オートマトン
ペトリネット
プロセス計算
確認用
Q. 形式的検証
参考
形式的検証 - Wikipedia
関連
Homotopy Type Theory(HoTT)
メモ
KLEE
tiny-regex-c/formal_verification.md at master · kokke/tiny-regex-c
#形式手法