Logic and Computation	THE AUTOMATA-THEORETIC APPROACH TO DESIGN VERIFICATION
Advanced course	MOSHE Y. VARDI Department of Computer Science, Rice University
First week	vardi@cs.rice.edu
Course description	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 nonemptiness 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.
Prerequisites	Basic familiarity with automata theory and logic will be assumed
Literature	No specific recommendation