Joao Marquez-Silva (University of Southampton), Towards More Efficient SAT-Based Model Checking

This talk addresses new techniques for the implementation of state-of-the-art model checking algorithms based on Boolean Satisfiability (SAT). First, the talk analyzes a number of key topics regarding the interface of the SAT solver with the model checker, namely the utilization of incrementality and clause learning and reuse. Afterwards, the talk addresses completeness conditions, and analyzes the utilization of interpolants. Finally, the talk concludes by describing optimizations to the utilization of interpolants.

• CV06
• Homepages:
  • Newton Institute
  • MPI Informatik
• Organizers:
  • Prof. Moshe Vardi
  • Prof. Andreas Podelski
• Invited Participants
• Application Form
• Search