Course: Automatic Verification (winter 2008)

Ofer Strichman

This course mainly coveres LTL Model Checking (the automata-based approach) and Bounded Model Checking. It also includes a lecture on testing. Specifically for my class I could not assume previous knowledge in logic and automata, and this is the reason that the relevant background in these topics is integrated in the course's material.

Acknowledgements: Some of the lectures were originally based on Doron Peled's text book and slides (see http://www.dcs.warwick.ac.uk/~doron/notes.html) . The DFA class is based on a presentation from CMU. Some of the slides in the testing class are based on several presentation I found several years ago on the web.

If you do not have textpoint installed, you will need to install two special fonts in windows to view the slides correctly: cmsy10.ttf and msam10.ttf

Note: some of the slides are hidden. I did not use these slides.

1. Introduction to verification and testing.
2. Propositional Logic.
3. Hoare Logic.
4. Temporal logic.
5. Deterministic Finite Automata.
6. Nondeterministic Finite automata and Buchi automata.
7. Checking emptiness of a Buchi automata.
8. Generalized Buchi automata.
9. Translating LTL to Buchi automata.
10. Model checking (Vardi-Wolper).
11. Bounded Model Checking.
12. SAT techniques.
13. Basic notions in testing.