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 symbol] BRICS WWW home page