「形式的検証」の版間の差分

編集の要約なし
(en:Formal verification(2012年5月3日 15:35:38(UTC))の翻訳(一部省略)をマージ)
第二の手法は論理的推論である。一般に [[:en:HOL (proof assistant)|HOL]]、[[:en:ACL2|ACL2]]、[[:en:Isabelle (proof assistant)|Isabelle]]、[[:en:Coq|Coq]] といった[[自動定理証明|定理証明]]ソフトウェアを使い、システムに関して形式的な推論を行う。この手法は完全自動化されていないのが一般的で、ユーザーの対象システムについての理解に応じて行われる。最近では、[[:en:Perfect Developer|Perfect Developer]] や Escher C Verifier といったツールが証明の完全自動化を試みている。
 
[[線形論理]]や[[時相論理]]などの[[非古典論理学|非古典論理]]は、モデル検査だけでなく論理的推論でも使われる。
 
=== ソフトウェアの形式的検証 ===