Parameterized systems are systems that involve numerous instantiations of the same finite-state module. Examples of parameterized systems include tele-communication protocols, bus protocols, cache coherence protocols, and many other protocols that underly current state-of-the-art systems.

Our interest in Parameterized Systems stems from the fact that these are infinite-state systems which still admit (in restricted cases) algorithmic analysis. As such, they are excellent testing grounds for exploring the fine border between algorithmic and deductive verification methods.

Formal verification of parameterized systems is known to be undecidable and thus cannot be automated. Recent research has shown that in many cases it is possible to use ABSTRACTION METHODS to generate a finite-state systems from a parameterized systems. The finite-state system can then be model-checked. If successful, it is possible to conclude that the original parameterized system satisfies its requirements. Otherwise, it is often the case that the counter-example produced by the model checker can indicate an error in the original parameterized system. This combined technique allows for automatic verification of parameterized systems.

The talk will describe some recent approaches that combine abstraction and model-checking to verify safety as well we liveness properties of parameterized systems. We start with the method of INVISIBLE INVARIANTS that combines a small-model theorem with an heuristics to generate proofs of correctness of parameterized systems. We also describe the method of NETWORK INVARIANTS which allows to explicitly describe a finite-system that, in a precise sense, has the same external behavior as an infinite-state one, and can be used for model-checking properties.

See: http://www.acm.org/awards/turing_citations/pnueli.html for Pnueli's Turing Award citation, and http://www.cs.nyu.edu/cs/faculty/pnueli/ for other information.