The talk 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.
Lenore Zuck teaches at the University of Illinois at Chicago. She spent several years as a program director at the National Science Foundation, where she was a member of the Trustworthy Computing program, the Software and Hardware Foundation program, and the Cyber Physical Systems program. Her background is in formal methods. Her recent work includes translation validation for LLVM, methodologies for automatic verification of infinite-state systems and applications of formal methods to security and privacy. Lenore Zuck has moved to UIC from NYU. Before that, she was on the Computer Science faculty at Yale University. Lenore Zuck holds a PhD in Computer Science from the Weizmann Institute of Science.
This talk is organized by the Cyber-Physical Systems Group at the Institute of Computer Engineering.