Deductive Verification of Reactive Systems
Instructor:
Amir Pnueli
Location: Ziskind 1
Time: Thursday, 11-13
The course will present methods for the deductive verification of reactive
systems, i.e. proving that reactive systems satisfy their specification,
given by Temporal Logic formulas, using deductive (i.e. theorem proving)
methods.
Unlike model checking, deductive verification is not restricted to
finite-state systems and can handle unrestricted programs with rich
data-structures. On the other hand, these techniques are not fully
automatic and require user interaction and ingenuity in the design of
auxiliary constructs such as invariants and ranking functions and,
at a later stage, the effective guidance of a theorem proving tool.
The course this year will concentrate on "hands-on" experience in
which the students will be required to verify small programs on a
variety of tools, such as PVS,
STeP,
SVC, and
TLV.
Lectures
-
Lecture 1 (14.5.02):
lecture1.pdf
-
Lecture 2 (23.5.02):
lecture2.ps,
lecture2.pdf
-
Lecture 3 (28.5.02):
lecture3.ps,
lecture3.pdf
-
A Brief Introduction to PVS:
brief.ps
-
A PVS Theory of Queues:
queue.pvs
-
A PVS Theory of Hotel Reservations:
reservation.pvs
-
Lecture 4 (6.6.02):
lecture4a.ps,
lecture4b.ps,
lecture4c.ps
-
Lecture 5 (13.6.02):
lecture5a.ps,
lecture5b.ps
-
Lecture 6 (20.6.02, revised 3.7.02):
lecture6.ps,
lecture6.pdf
-
Lecture 7 (4.7.02, revised 10.7.02):
lecture7.ps,
lecture7.pdf
-
Lecture 8 (11.7.02):
lecture8.ps,
lecture8.pdf
-
Lecture 9 (18.7.02):
lecture9.ps,
lecture9.pdf
-
Additional Material (1.1.03):
additional.ps,
additional.pdf
Term Project
TLV Resources
Amir Pnueli
<amir@wisdom.weizmann.ac.il>
Last modified: Wed Jan 1 2003