Verification via Model Checking


Model checking is a general term for a collection of related formal methods. Specification of program behavior is done in a modified predicate calculus called Temporal Logic. A Model is made that represents the salient features of a program, and the model is "checked" to see if the temporal logic specs are true or not for the model.

The techniques are applicable to all programs, but are especially useful for concurrent computations.

Symbolic Model Checking reference.

Your Assignment (not applicable Spring 2009)

Here are details on the algorithm and the data for running it

This information shows the basic model structure used by Clark's early model check "mcb".

To run this model check and try some assertions, log onto uncle-leo.cs.unc.edu (which one of our few remaining sparc machines). Here are the models, the checker, and instructions.


Reference


The software source

You may get a copy of Ed Clarke's model checker to mess with for yourself. (the binaries are for a sparc, so log onto a Sun somplace or recompile it for your platform).


Algorithm Details

There are several major phases of activity to program: