2012年9月7日 (金) 03:30時点における版編集 Melan (会話 \| 投稿記録) 25,487 回編集 en:Formal verification（2012年5月3日 15:35:38(UTC)）の翻訳（一部省略）をマージ ← 古い編集		2012年11月4日 (日) 08:59時点における版編集取り消し MetaNest (会話 \| 投稿記録) 拡張承認された利用者 21,577 回編集編集の要約なし新しい編集 →
15行目: 第二の手法は論理的推論である。一般に [[:en:HOL (proof assistant)\|HOL]]、[[:en:ACL2\|ACL2]]、[[:en:Isabelle (proof assistant)\|Isabelle]]、[[:en:Coq\|Coq]] といった[[自動定理証明\|定理証明]]ソフトウェアを使い、システムに関して形式的な推論を行う。この手法は完全自動化されていないのが一般的で、ユーザーの対象システムについての理解に応じて行われる。最近では、[[:en:Perfect Developer\|Perfect Developer]] や Escher C Verifier といったツールが証明の完全自動化を試みている。 [[線形論理]]や[[時相論理]]などの[[~~非古典論理学\|~~非古典論理]]は、モデル検査だけでなく論理的推論でも使われる。 === ソフトウェアの形式的検証 ===

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