Advanced Model Checking
Summer Semester 2017
This lecture is about algorithms for SAT and also touches on applications of SAT to model checking and related problems.
The lecture takes place Wednesdays from 8:30 to 10:00 in room S3 048.
Version 2016.1 of the slide set is available as amcslides.pdf.
Donald Knuth, The Art of Computer Programming (TAOCP) Volume 4, Fascicle 6: Satisfiability, Addison-Wesley, December 8, 2015 (Volume 4B, Pre-fascicle 6A: A Draft of Section 22.214.171.124: Satisfiability).
You find a description of the Plaisted-Greenbaum polarity based encoding in our recent TACAS paper.
SMVFlatten tool to flatten SMV models.