Lenore D. Zuck

Date: 15:30, Thursday, November 27, 2014
Speaker: Lenore D. Zuck
Venue: TU Vienna

15:30 !

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.

Posted in RiSE Seminar