Modern SMT Solvers Are SAT Solvers Enough?

• Software engineering (SE) problems reduced to logic problems • Automation, engineering, usability of SE tools through solvers High-level description of the SAT/SMT problem & logics • Rich logics close to program semantics • Demonstrably easy to solve in many practical cases Modern SAT solver architecture & techniques • DPLL search, shortcomings • Modern CDCL SAT solver: propagate (BCP), decide (VSIDS), conflict analysis, clause learn, backJump, • Termination, correctness • Big lesson: learning from mistakes Topics covered in Lecture 2 • Modern SMT solver architecture & techniques • Rich logics closer to program semantics • DPLL(T), Combinations of solvers, Over/under approximations • My own contributions: STP & HAMPI • Abstraction-refinement for solving • Bounded logics • SAT/SMT-based application