C言語検証 - gcg00467

思い立って，C言語の検証関係を調べてみた．まだまだ調査は足りない．

Wikipediaの「静的コード解析」のページから

http://ja.wikipedia.org/wiki/静的コード解析

BLASTとSLAM

もちろん，BLAST と SLAM はある．
SLAMは Wikipedia にはでていない....

VARVEL

• NECの検証ツール．2009年発売予定??
• 基本的には有界モデル検査. ただし，assertion, pre/post condition も書けるように拡張している．静的解析を併用して探索空間を少なくする，といった工夫があるらしい．
• 以前は，F-test と言っていた．

F. Ivancic et al：Model checking C programs using F-Soft. Invited. paper in the Proceedings of the IEEE International Conference on. Computer Design (ICCD), October 2005.
http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1524168

橋本ほか: 形式手法によるC言語検証ツール 「VARVEL」
http://www.google.com/search?client=opera&rls=ja&q=Model+Checking+C+Programs+Using+F-SOFT&sourceid=opera&ie=utf-8&oe=utf-8

QAC

メーカーのウェブページ
http://www.programmingresearch.com/QAC_MAIN.html#1_4
を見た感じだと，コーディングスタンダードをenforceする，ということみたい．

Coverity

Coverity (http://www.coverity.com/) は会社の名前．
製品は，Coverity Prevent for C/C++ など，いろいろある．
原理がちゃんと書いてあるものは見つからなかったが，以下のようなことができる，
と書いてある．

Concurrency Issues
. Double locks, missing locks
. Locks acquired in incorrect order
. Locks held by blocking functions
Memory Corruption and
Mismanagement
. Resource leaks
. Calls to freeing functions using
invalid arguments
. Excessive stack use in memoryconstrained
systems
Crash-causing pointer errors
. Dereference of null pointers
. Failure to check for null return values
. Misuse of data contained within
wrapper data types

CQUAL

型推論ベースのC言語検証ツール．
http://www.cs.umd.edu/~jfoster/cqual/
2004年以来更新されていない．

Caduceus

おなじみの Caduceus．
http://caduceus.lri.fr/

Review-C

NEC のツール．http://rec.ncos.co.jp/
コーディングスタンダードからの逸脱の指摘が中心で，
あまり難しいことはできないようだ．

CBMC

Clarke先生のところの，C Bounded Model Checker．
http://www.cs.cmu.edu/~modelcheck/cbmc/
これも開発は止まっているようだ．