__Course: Automatic
Verification (winter 2008)__

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.

- Introduction to verification and testing.
- Propositional Logic.
- Hoare Logic.
- Temporal logic.
- Deterministic Finite Automata.
- Nondeterministic Finite automata and Buchi automata.
- Checking emptiness of a Buchi automata.
- Generalized Buchi automata.
- Translating LTL to Buchi automata.
- Model checking (Vardi-Wolper).
- Bounded Model Checking.
- SAT techniques.
- Basic notions in testing.