Automatic deductive verification with invisible invariants

Abstract

The paper presents a method for the automatic verification of a certain class of parameterized systems. These are bounded-data systems consisting of N processes (N being the parameter), where each process is finite-state. First, we show that if we use the standard deductive INV rule for proving invariance properties, then all the generated verification conditions can be automatically resolved by finite-state (BDD-based) methods with no need for interactive theorem proving. Next, we show how to use mo del-checking techniques over finite (and small) instances of the parameterized system in order to derive candidates for invariant assertions. Combining this automatic computation of invariants with the previously mentioned resolution of the VCs (verification conditions) yields a (necessarily) incomplete but fully automatic sound method for verifying bounded-data parameterized systems. The generated invariants can be transferred to the VC-validation phase without ever been examined by the user, which explains why we refer to them as "invisible". We illustrate the method on a non-trivial example of a cache protocol, provided by Steve German. © Springer-Verlag Berlin Heidelberg 2001.