[  contents | resources ]

Advanced Model Checking

Summer Semester 2012

Armin Biere

Contents

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

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

Resources

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.

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