Event Details
Automated Verification = Graphs, Automata, and Logic
Presenter: Dr. Moshe Vardi
Supervisor: Bruce Kapron
Date: Thu, February 8, 2001
Time: 15:30:00 - 00:00:00
Place: D288 MacLaurin Bld.
ABSTRACT
Abstract:
In automated verification one uses algorithmic techniques to establish the correctness of the design with respect to a given property. Automated verification is based on a small number of key algorithmic ideas, tying together graph theory, automata theory, and logic. In this self-contained talk I will describe how this "holy trinity" gave rise to automated-verification tools.
Biography:
Moshe Y. Vardi is Karen Ostrum George Professor in Computational Engineering and Chair of Computer Science at Rice University. His interests focus on applications of logic to computer science, including database theory, finite-model theory, knowledge in multi-agent systems, and design specification and verification.
He recently received the 2000 Godel Prize, which recognizes outstanding papers in the area of theoretical computer science. He received this prestigious honor for his paper, "Reasoning about infinite computations," which he co-authored with Pierre Wolper of Universite de Liege. This paper established the foundations for new approaches to formal verification.
Vardi received his Ph.D. from the Hebrew University of Jerusalem in 1981. Dr. Vardi has served as the general chair for LICS and the Federated Logic Conference, and is the general chair for the SPIN 2001 Workshop on Model Checking of Software. He is an author of the book "Reasoning about Knowledge," an editor of SIAM Journal on Computing and ACM Transactions on Database Systems, and an ACM Fellow.
Followed by a reception at the Faculty Club
If you would like to meet with Moshe, please contact Bruce at bmkapron@csr.uvic.ca