SystemX Affiliates: login to view related content.
I will give an introduction to Satisfiability Modulo Theories (SMT) solvers, including the DPLL(T) architecture that combines a Boolean satisfiability (SAT) solver with a theory solver, techniques for building individual theory solvers, and techniques for theory combination. I will also cover some applications of SMT solvers, including symbolic execution and equivalence checking.
Clark Barrett joined Stanford University as an Associate Professor (Research) of Computer Science in September 2016. Before that, he was an Associate Professor of Computer Science at the Courant Institute of Mathematical Sciences at New York University. His expertise is in constraint solving and its applications to system verification and security. His PhD dissertation introduced a novel approach to constraint solving now known as Satisfiability Modulo Theories (SMT). Today, he is recognized as one of the world's experts in the development and application of SMT techniques. He was also an early pioneer in the development of formal hardware verification: at Intel, he collaborated on a novel theorem prover used to verify key microprocessor properties; and at 0-in Design Automation (now part of Mentor Graphics), he helped build one of the first industrially successful assertion-based verification tool-sets for hardware. He is an ACM Distinguished Scientist.
