Date:
15:30,
Thursday, November 27, 2014
Speaker:
Lenore D. Zuck
Venue: TU Vienna
Notes:
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.
