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
