### Automata-Theoretic Approach to Automated Verification

**Moshe Y. Vardi**

Rice University

Lecture 1

Lecture 2

Lecture 3

Lecture 4

Lecture 5

The automata-theoretic approach to design verification uses the theory
of automata as a unifying paradigm for design specification,
verification, and synthesis. Both designs and specifications are in
essence descriptions of computations. These computations can be viewed
as words or trees over some alphabet. Thus, designs and specifications
can be viewed as descriptions of languages over some alphabet. The
automata-theoretic perspective considers the relationships between
designs and their specifications as relationships between languages. By
translating design and logical specifications to automata, questions
about programs and their specifications can be reduced to questions
about automata. More specifically, questions such as satisfiability of
specifications and correctness of designs with respect to their
specifications can be reduced to questions such as non-emptiness and
containment of automata.

Unlike classical automata theory, which focused on automata on finite
objects, the applications to design specification, verification, and
synthesis, use automata on infinite objects, since the computations in
which we are interested are typically infinite. The course will provide
an introduction to the theory of automata on infinite objects and
demonstrates its applications to design specification, verification,
and synthesis.