Parameterized Verification: Theory and Practice

As a part of the RiSE seminar series, the Institute of Information Systems hosted a talk by Lenore D. Zuck.

ABSTRACT

The will provide with a background on automatic generation of invariants and other constructs used in verification parameterized systems (for safety proofs, this method is sometimes referred to as "Invisible Invariants".) Two "real-life" case studies will be described, one in which the theory sufficed to verify, and find a flaw ("bug") in a hurricane prediction system, and one in which the theory had to be augmented by a compositional construct to verify the correctness of a satellite system.