C言語によるCBMC(有界モデル検査技術)を使用したPDD(証明駆動開発)

C言語によるCBMC(有界モデル検査技術)を使用したPDD(証明駆動開発)を藤倉さんが提唱されている。
http://tfujikura.blogspot.com/search/label/PDD
OCaml似の文法を使用するCoqによる証明駆動開発に比べて、c(c++)言語で仕様を書けるのでとてもわかりやすいと思う。
http://d.hatena.ne.jp/garyo/20110301
CBMC-PDDについて色々調べてみたいです。

CBMC (Bounded Model Checking for C/C++)は以下でWindows版、Linux版などがダウンロードできます。
http://www.cprover.org/cbmc/
簡単な使い方は島さんのブログがわかりやすいです。
http://saltheads.blog134.fc2.com/blog-entry-1.html