Deciding whether a logical formula has a solution is at the heart of many verification tools, from bounded model checking to symbolic execution. Satisfiability modulo theories (SMT) solvers answer this question for formulas over arithmetic, arrays, bit-vectors and uninterpreted functions, and they have become a standard back end for program analysis. This talk introduces how SMT solvers work, starting from propositional SAT solving and moving to first-order theories and the specialized procedures that decide them. It discusses how a SAT solver and theory solvers cooperate to handle the Boolean structure of a formula, and how solvers for different theories can be combined.

Understanding what a program does is a fundamental problem, especially for computer security. In this talk, I will give an overview of research in our group on reasoning about program behavior, ranging from static program analysis and logic-based approaches over testing to machine-learning techniques. I will discuss how semantic properties can be used to detect malicious behavior, how we can recover information that has been lost during compilation, and how learning-based methods can help when precise models of program behavior are difficult to construct. Along the way, I will highlight some of the challenges that arise when applying these techniques to real-world software, including scalability, incomplete information, and changes in software and data over time.