6th International School on Rewriting
July 16th - 20th, 2012. Valencia, Spain
SAV: SAT and SMT Techniques in Proof and Verification
Propositional satisfiability does not only lie at the heart of the most important open problem in complexity theory (P vs. NP), it is also at the basis of many practical applications. In the last couple of decades, areas such as Electronic Design Automation, Verification, Artificial Intelligence and Operation Research have successfully used SAT-based techniques for solving some of their problems.
However, propositional logic is probably not the most appropriate language for expressing complex domain-specific constraints. For that reason, an extension of SAT called SMT was developed in order to combine propositional reasoning with domain-specific reasoning (e.g. arithmetic, bit-level reasoning or inductive data types). Currently, SMT solvers are being increasingly used in all sort of practical applications due to the expressivity of their input language and their efficiency.
In this course we will give an overview of SAT and SMT solving. We will first focus on the Conflict-Driven Clause Learning (CDCL) algorithm for SAT, and the DPLL(T) approach to SMT, highlighting the key points that are responsible for their practical success. Then, we will give some illustrative examples of where and how this technology is used in several verification efforts.
