SAT and SMT Solvers: A Foundational Perspective

Speaker: Vijay Ganesh

Abstract

Over the last two decades, software engineering (broadly construed to include verification, testing, analysis, synthesis, security) has witnessed a silent revolution in the form of SAT and SMT solvers. These tools are now integral to many analysis, synthesis, verification, and testing approaches. In my lectures, I will trace the important technical developments that underpin SAT and SMT solver technology, provide a detailed explanation of how they work, provide a proof complexity-theoretic view of solvers as proof systems, and describe how users can get the most out of these powerful tools.