Automata-Theoretic Verification
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.
Funding is available for graduate students interested in
working on this project.
Back to Algorithms & Complexity page
To the Computer-Aided Verification and Formal Methods page