Advanced Model Checking
Summer Semester 2011
Last lecture June 29.
Oral exam should be scheduled individually.
This lecture is about algorithms for SAT and applications of SAT to model checking and related problems.
Version 2011.6 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 background material consider the Handbook of Satisfiability.
SMVFlatten tool to flatten SMV models.