Philipp Rümmer
Associate Professor at the IT Department of Uppsala University, Sweden
Overview
Satisfiability Modulo Theories, or SMT, describes a class of constraint solvers that are developed primarily for the purpose of program verification. SMT solvers combine efficient solvers for Boolean constraints, known as SAT solvers, with procedures for a wide range of theories and data types, including different forms of arithmetic, uninterpreted symbols, arrays, algebraic data -types and co-data-types, and strings. SMT solvers are widely applied in different verification applications, for instance deductive verification systems, model checkers, bounded model checkers, and white-box fuzzers. The presentation will give a high-level introduction of the algorithms, architecture, and use of SMT solvers, and outline in particular the application of SMT for security analysis.
Biography
Philipp Rümmer is an Associate Professor at the IT Department of Uppsala University, Sweden. He received his PhD from Gothenburg University in 2008, and is generally interested in any kind of technology that is useful for program verification. Over the years, he has contributed to deductive verification methods (including the tools KeY and Boogie), developed software model checkers (including Eldarica and JayHorn), worked on theorem provers and SMT solvers (leading to a zoo of solvers, among others inhabited by Princess, Norn, Sloth, Ostrich, Trau, UppSAT), and investigated the application of verification methods in domains like Embedded Systems and Security.
Video