TU Wien Informatics

20 Years

Parameterized Verification: Theory and Practice

  • 2014-11-27
  • Research

The talk will provide with a background on automatic generation of invariants and other constructs used in verification parameterized systems.

Abstract

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.

Biography

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.

Note

This talk is organized by the Cyber-Physical Systems Group at the Institute of Computer Engineering.

Speakers

  • Lenore D. Zuck, Department of Computer Science, University of Illinois at Chicago, USA

Curious about our other news? Subscribe to our news feed, calendar, or newsletter, or follow us on social media.

Note: This is one of the thousands of items we imported from the old website. We’re in the process of reviewing each and every one, but if you notice something strange about this particular one, please let us know. — Thanks!