| Project: | Automata-Theoretic Verification |
| Contact: |
Moshe Y. Vardi |
| WWW page: | not available |
| Description: |
Automata-Theoretic Verification uses the theory of automata as an
unifying paradigm for program specification, verification, and
synthesis. Both programs and specifications are in essence
descriptions of computations. These computations can be viewed as
words over some alphabet. Thus, programs and specifications can be
viewed as descriptions of languages over some alphabet.
The automata-theoretic perspective considers the relationships between programs and their specifications as relationships between languages. By translating programs and 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 programs with respect to their specifications can be reduced to questions such as nonemptiness and containment of automata. This project investigates several applications of automata theory to specification, verification, and synthesis. |