Advanced Model Checking

Summer Semester 2010

Oral exams have to be scheduled invidually.

This lecture is about algorithms for SAT and applications of SAT to model checking and related problems.

Version 2010.3 of the slide set is available as amcslides.pdf.

All topics are relevant until and not including interpolation.

The two parts on interpolation and full LTL encodings is supplimentary and can be skipped.

You find a description of the Plaisted-Greenbaum polarity based encoding in our recent TACAS paper.

As further background material consider the Handbook of Satisfiability.