Automata-Theoretic Approach to Automated Verification
Credit:
-
Read
this to receive credit in this course.
Current Assignments:
Assignment 8
Instructors:
Amir Pnueli
and
Moshe Y. Vardi
Location: Ziskind 1
Time: Wednesday, 9:15-12, Oct. 28, 1998 - Feb. 10, 1999
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.
Topics to be covered include:
Reading:
There is no textbook that covers the material of the course.
Relevant papers will be distributed to the students during the course.
In addition, official lecture notes, taken by the students,
will be posted on this page.
Credit:
The course carries 3 units of credit.
Final grade will be based on:
Students
Lecture Notes
Assignments
Auxiliary Readings
Special Accomodation:
Any student with a disability requiring a special accomodation in this class
is encouraged to contact the instructors.
Links