dar seminar - Amir Pnueli, Friday 11am in CS seminar room

This week's seminar is moved to Fri 11am, in the same CS seminar room.
So, there is no seminar today.

Our speaker will be Prof. Amir Pnueli, winer of the 1996 Turing Award.

I will send out an abstract after I get it.

Prof. Pnueli will be visiting us as the speaker at our distinguished
lectuer's series on Friday (at 2pm in Harriman Hall 108---see his talk
abstract below).  Prof. Pnueli has been an invited speaker at many
conferences and occasions.  We are lucky to have him also give a more
special, less formal talk in the dar seminar.

        Taming the Infinite: Verification of Parameterized Systems

                             Amir Pnueli

          Weizmann Institute of Science and New York University

The task of formal verification sets out to establish with
mathematical certainty that a reactive (hardware or software) system
conforms with its specification. Two main paradigms are currently
applied for performing this important task: MODEL CHECKING which, in a
fully automatic manner, exhaustively explores all the reachable states
of the system but is restricted to systems with a finite (and not too
large) number of states, and DEDUCTIVE VERIFICATION, which requires
user ingenuity and guidance, but can be applied to infinite-state

In this talk, we will survey approaches which combine ideas from the
two methods to achieve higher degrees of automation in the
verification of infinite-state systems. After exploring the various
sources for infinity within systems, which could be due to complex
control or architectural structure or due to extensive data, we will
identify the main techniques proposed to deal with this "state
explosion", and can be used to reduce an infinite-state system into a
finite one. These include the techniques of abstraction,
(de)composition, reduction due to symmetry, and generic
instantiation. Typical successful applications of these techniques are
the uniform verification of parameterized systems, where we consider
a family of networks whose size (e.g. number of processes) is a
parameter, and the method is able to establish its correctness for any
value of the parameter.