Model-Checking C Programs against JML-like Specification Language

Model checkers achieved a great success in verification of control-flow properties such as reach ability of error states, but few of them are capable of handling data structural properties such as ``the procedure preserves the sorted ness of linked lists''. On the other hand, specification languages like Java Modeling Language (JML) can express such property, and deductive verification tools like Spec# and Frama-C can prove properties expressed in such language. But these tools in general do not produce counter-examples when the proof attempts fails. This paper proposes a bounded model checker CForge and its specification language, aiming in the middle of these two approaches. The language has JML-like syntax extended with C-specific constructs and is designed to be suited for model checking. This allows writing data structural properties neatly using quantifiers, relational operations, etc., while enjoying the benefit of model checkers. As an experiment, we wrote specifications for ten programs, each of which contained one non-trivial bug such as a sorting failure, wrong manipulation of a linked list, etc. and checked them using CForge. CForge detected seven out of the ten bugs. The result shows that our language and tool are capable of specifying and checking complex properties.