SMT/SATソルバーとモデルチェッカー

Question

最近、私は正式な検証技術を研究し始めました。文献では、モデルチェッカーとソルバーが何らかの意味で使用されています。 しかし、モデルチェッカーとソルバーはどうつながっていますか？

p.s.いくつかの論文やリンクが提案されていれば幸いです。

Answer 1

モデルチェックを実行するには到達可能性解析が必要であり、これを行うにはプログラムの遷移が記号的に実行されることがよくあります。結果の満足度問題の解は、ソルバーによって作成されます。

http://leeseshia.org

エドワードA.リーとSanjit A. Seshia、組込みシステムの概要、サイバー：非常に基本的な、非常に良い導入は、このフリーテキストブック（：分析と検証パートIII）で発見されました物理システムアプローチ、第2版、MIT Press、ISBN 978-0-262-53381-2、2017

Answer 2

モデルチェックでは、モデルと仕様（またはプロパティ）があり、モデルが仕様。

SAT解答では、数式があり、それに満足のいく代入を見つけようとします。

モデルチェックでは、モデルとプロパティの否定を結びつけて1つの数式を与えることができます。この式を解くにはソルバを使用します。それがあなたに解決策を与えるならば、プロパティが時々違反されることを意味するでしょう（否定されたプロパティを結びつけたので）。 unsatを取得すると、モデルがプロパティ/仕様を満たしていることを意味します。