Systems and Software Verification

前掲の本と一緒に購入したのがこの洋書です。どこかで紹介されていたので、ふとした気まぐれで購入してみたのですが、これが大当たりでした。

Clarke 先生の "Model Checking" は内容がぎっしり詰まっているため、理解しながら読み進めるのにかなりのエネルギーが必要なのですが、こちらは190ページほどの少ないページ数で要点だけをしっかりまとめて書いていますので、重要な部分をしっかりと確認することができます。

CTL と LTL の表現力の違いとか、検証するためのアルゴリズムについての話などが、ピンポイントで適切な例とセットで記述されており、読んだだけですっと頭に入ってくる良書でした。なお、後ろ半分は SPIN や SMV などのツールの解説です。

ただ、一度理解したことがある人間が復習用として読んだから非常に分かりやすかっただけかもしれません。結局は Clarke 先生の本と両方を同時に読み進めるのが一番理解が深まるかもしれませんね。