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.