# CAVEAT: technique and tool for computer aided verification and
transformation

**Pascal Gribomont **

Didier Rossetto

**In TACAS, pages
216--229**

### Abstract:

*We describe CAVEAT, a technique and a tool (under
development) for the stepwise design and verification of nearly finite-state
concurrent systems, whose most variables are boolean. The heart of CAVEAT is a tool for verifying (inductive) invariants. The underlying method
is classical: formula ***I** is an invariant for system if and only
if some formula is valid. CAVEAT uses the * connection
method* to extract from a (small) set of * paths*
(some kind of assertions) about the non-boolean variables; is valid
if and only if all paths contain * connections*, i.e., are inconsistent.
For typical systems given with a correct invariant, the formula is
rather large but is quite small. The second part of CAVEAT (not
implemented yet) supports an incremental development method that is fairly
systematic, but has proved to be flexible enough in practice.

** Comments**

University of Liège, Belgium.

Available as * PostScript*,
* DVI*.

BRICS WWW home page