[Prev][Next][Index]

dar seminar - Pnueli: Verifying Parameterized Systems with Invisible Invariants

This is the special seminar tomorrow morning at 11am in the CS seminar
room.  Everyone is welcome, and please be on time!


		 Design and Analysis Research Seminar
                         Fri., Nov. 2, 2001
                    11am-12pm, CS Seminar Room 1306

       Verifying Parameterized Systems with Invisible Invariants

                            Amir Pnueli

         Weizmann Institute of Science and New York University

This work is part of a continuing effort to unify the powerful (but
interactive) method of deductive verification with the restricted (but
automatic) method of model checking. Typically, there are two
difficulties in the application of deductive verification. The first
is the generation of the auxiliary constructs (invariants and ranking
functions), while the second is the validation of the verification
conditions.

At first, we show that the verification conditions generated for a
wide class of parameterized systems, are of the AE canonic form and
can, therefore, be validated by a BDD tool over finite instances of
these systems. This leads to automation of the second step in
deductive verification.

Then, we outline a heuristic for the automatic generation of inductive
assertions for a compatible class of parameterized systems. Once these
are generated, we can apply the automatic validation method to
establish the correctness of the property. When these two steps can be
performed by a single tool (which we describe), the user never gets to
see the automatically generated auxiliary assertions, which explains
the name "Verification by Invisible Invariants" associated with the
method. We will illustrate the application of this method on a cache
protocol provided by Steve German.