モデル検査アプリケーションを導出して構築する本を探しています

Question

プログラム検証を独学で勉強中です 証明アシスタント. 。私はその本を持っています 実践的な論理と自動推論のハンドブック これは、そのようなシステムを理解するために必要な証明を提供しますが、私にとってより重要なのは、次のような必要なアルゴリズムの実装も提供します。 OCAMLソース.

にリストされているツールの一部は、 ウィキペディア:モデルチェックツール そして ヤホダ：検証ツールデータベース はオープンソースですが、理論、証明、アルゴリズム、ソース コードが同時に提示され、相互に強化され、最終的なアプリケーションに至るまでの段階的な構築が行われる方が私は好みます。

モデルチェックのためのそのような本はありますか?

編集

探しているものが見つかるかも知れません コンピュータサイエンスのための数理論理学 と プロローグのソース. 。私はその本を持っていないので、この本が要件を満たすかどうか知っている人はいますか?

Answer 1

ジョン・ハリソンの本は、理論から実践までを一貫して行っており、すべてのソースコードが利用可能であるという点で例外的です。モデル検査に関する同等の本を見つけるのは難しいと思いますが、ほぼ同等の本がいくつかあります。

• モデル検査の原則 Baier と Kataen の著には、多くの例とかなり詳細なアルゴリズムの説明が含まれています。
• SPIN モデル チェッカー Gerard Holzmann によるこの手法は、初期のモデル チェッカーの 1 つの作者とはまったく異なる扱いです。彼はこのツールを約 30 年間保守しており、「プログラマティック」アプローチを採用しています。

オンラインで利用できる一部のコースのコースノートとラボの課題に従うほうがよいでしょう。たとえ本にまとめられていないとしても、少なくとも理論、実践、例は見つかります。

• CMU でのエドモンド・クラークのコース には、いくつかの異なるモデル チェッカーのチュートリアルを含むリーディング リストがあります。
• Joost-Pieter Kataen のソフトウェア検証コース そしてその続報 実用モデルの検査 そして 高度なモデルチェック 多くの地面を覆います。

最後に、これは完全にあなたが求めているものではありませんが、あなたはロジックを勉強し、現在はモデル チェックを勉強しているため、静的プログラム解析の基礎であり、モデル チェックと密接に関係している抽象解釈への言及に必ず遭遇します (ただし、この関係は、モデルチェックの文献では必ずしも明示されているわけではありません)。

• パトリック・クーゾのMITコース は、格子理論の基礎から単純な言語用の静的アナライザーの完全な実装まで、あらゆるものをカバーする強力なツールです。彼のコース教材にはすべてのコードと演習が含まれています。