Copper Manual, Tutorial, and Specification Grammar

Copper is a software model checker. It enables you to verify properties against C source code. Copper is also fairly versatile in the kinds of claims it can check. On one hand, it can look for simple errors such as assertion violations. On the other hand, you can use Copper to check more complicated specifications expressed as finite state machines or linear temporal logic formulas. Copper also supports the verification of multi-threaded programs where the threads communicate with each other via shared variables, or handshakes, or both. Finally, while Copper uses explicit-state verification by default, it can be used to perform symbolic BDD-based verification by techniques described in the section on "Symbolic Verification."

Copper has some limitations. In particular, Copper does not support non-integral basic data types such as floats and doubles. It treats all variables of such unsupported types as integers. Copper also treats pointers in an unsound manner. In practice, this means that the result of running Copper on a pointer-manipulating program cannot be trusted in general. Copper is still useful as a bug-finding tool on such programs, however. In addition, Copper treats integers as unbounded quantities by default. Allowing unbounded integers is, in general, unsound because integers are represented as bit-vectors in practice. This is usually not a big issue but can be avoided by techniques described in the tutorial. Finally, Copper is unable to handle recursive programs by default since it uses inlining. Techniques to verify recursive programs with Copper are also described in the tutorial.

The manual and tutorial refer to the following files, which are included in the PDF:

• dp-2.pp
• dp-2.spec
• dp.2.ce
• dp.2.txt
• philosopher.1.txt
• philosopher.2.ce
• philosopher.2.txt
• philosopher.5.ce
• philosopher.pp
• philosopher.spec