[  news | contents | resources ]

Advanced Model Checking

Summer Semester 2017

Armin Biere

News

no news

Contents

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.

Resources

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 7.2.2.2: Satisfiability).

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

As background material consider the Handbook of Satisfiability (see also the tutorial page of the SAT association).

The SAT Association, the SAT conference, and the SAT Competition.

Further related papers are listed on our publication page, additional software, particularly SAT solvers, can be found on our software page

SMVFlatten tool to flatten SMV models.