CAVEAT: technique and tool for computer aided verification and
In TACAS, pages
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.
University of Liège, Belgium.
Available as PostScript,
BRICS WWW home page