Automated Verification = Graphs, Automata, and Logic

      Moshe Y. Vardi
    Rice University

   SF1105, 11am March 2, 1998

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.



Moshe Y. Vardi is a Noah Harding Professor of Computer Science and
Chair of Computer Science at Rice University.  Prior to joining Rice in
1993, he was at the IBM Almaden Research Center, where he managed the
Mathematics and Related Computer Science Department.  His research
interests include database systems, computational-complexity theory,
multi-agent systems, and design specification and verification.  Vardi
received his Ph.D. from the Hebrew University of Jerusalem in 1981. He
is the author and co-author of over 100 technical papers, as well as a
book titled "Reasoning about Knowledge".  Vardi is the recipient of 3
IBM Outstanding Innovation Awards.  He is an editor of several
international journals and currently serves as the General Chair of the
Federated Logic Conference.