April 18, 2007: Seminar: Lenore Zuck: "Automatic Verification of Parameterized Systems"

Seminar Announcement

Automatic Verification of Parameterized Systems

Lenore Zuck
Associate Professor,
University of Illinois at Chicago
Wednesday, April 18, 2007

3:00 p.m., Room 627 SEO

Abstract:

The talk will briefly introduce the area of automatic formal verification, the challenges posed when attempting to automatically verify infinite-state systems, the notion of "parameterized systems", and the importance and implications of their automatic verification. The talk then will present three newly developed methodologies to deal with the task:

(1) The method of "Invisible Invariants" that automatically verifies safety properties of parameterized systems, which has been tested on a wide variety of systems.

(2) The method of "Counter Abstraction" that applies a well-studied abstraction technique in novel ways to automatically verify liveness properties of parameterized systems.

(3) A simple variant of the method of "Network Invariants" that is applicable to automatic proofs of liveness properties of a wide range of parameterized systems.

The types of systems that can be verified by these methods include cache and communication protocols, processor pipelines, and high-level program specifications. These applications will briefly be discussed in the talk as well.