Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
This lecture introduces Satisfiability Modulo Theories (SMT) solving, focusing on determining truth values for complex formulas involving propositional logic and uninterpreted functions. It covers the flattening and extraction of propositional structure, handling function symbols and arithmetic, the theory of uninterpreted function symbols, decision procedures in SMT solvers, and quantifier instantiation during the solving process.