Fast SAT Solvers and Practical Decision Procedures

Instructor Edmund Clarke

Seminar in Programming Languages: Model Checking

 

This course will focus on fast propositional satisfiability solvers and practical decision procedures (Presburger arithmetic, the theory of reals with and without multiplication, the theory of lists and arrays, etc.) and their application to model checking, automated theorem proving, program verification and program analysis.

The course will be self-contained although some knowledge of propositional and predicate logic will be helpful. In particular, no previous knowledge of model checking will be required. Students will be expected to give a lecture or do a course project.

Schedule:  Fridays 12:00pm—1:20pm

Location:   Wean Hall 4623