TL;DR Go でモデル検査器を実装しながら形式手法を学ぶ本である。 既存のツールを使うだけでは見えにくい、背後にある理論や動作原理を、動作する完全なソースコードを書きながら体感的に学べる。 対象読者 形式手法を、ツールの利用者としてではなく、ツールを作る側から理解したい人向けの本である。形式手法には大きく分けて定理証明とモデル検査があり、本書はモデル検査を扱う。 関連 形式手法 モデル検査 定理証明 Go 技術書典の頒布ページ