CCC, the CASL Consistency Checker, is a tool to prove the consistency of specifications written in the algebraic specification language CASL (see the CoFI pages for further information concerning this language), i.e. to show that the specification has at least one model.

The CCC is based on a calculus presented here. Its strategy for consistency proofs is as follows: guided by the structure of the specifiation text, one splits up the original proof goal by applying certain proof rules into simpler properties, avoiding the need to construct (and prove) actual models of specifications as far as possible.

CCC is a faithful implementation of this consistency calculus. It is based on a logical core, representing the rules of the calculus. On top of this core, a body of derived rules and tactics is built. Moreover, CCC offers proof management and a number of specialized static checkers, as well as a connection to the CASL proof tool HOL-CASL which facilitates discharging proof obligations.


You can download CCC in various packages:


After downloading, unpack CCC in a directory of your choice (all tar archives will unpack into a directory called ccc), cd into that directory and do
./configure [options]
to configure CCC. Options are only needed if you want to configure the source package, the binary version does not need options (but it needs to be configured!): To build CCC, cd to the directory ccc/src, and do
./build [HOL-CASL | ttt | clean ]
You'll need CATS and HOL-CASL, and Isabelle 99-2 (see under download, past releases). To run CCC, use ccc/bin/ccc. See the file ccc/INSTALL for further information.

The Files


A paper describing the foundations of CCC: