###
Automated Verification = Graphs, Automata, and Logic

Moshe Y. Vardi

Rice University
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.
I will then describe two research efforts currently taking place
at Rice. The first effort attempts to improve the fair-path algorithm,
which is a key algorithm in symbolic model checking and is often a
computational bottleneck. The second effort attempts to address the
state-explosion problem by reducing the state space with respect to
the verified property.