Advances in Automated Theorem Proving: Symbolic Automata, Nonlinear Arithmetic over the Reals, and Fixpoint Calculation

Thomas Ball

Microsoft Research, Redmond, Washington

http://research.microsoft.com/~tball

Abstract
In the last decade, advances in satisfiability-modulo-theories (SMT) solvers have powered a new generation
of software tools for verification and testing. These tools transform various program analysis problems into
the problem of satisfiability of formulas in propositional or first-order logic, where they are discharged by
SMT solvers, such as Z3 from Microsoft Research (MSR). In this talk, I'll review advances from MSR that
expand the scope of SMT solvers on several fronts, including:

  • symbolic automata, which lift classical automata analyses to work modulo symbolic constraints on alphabets enabling the precise analysis of programs that manipulate strings;
  • nonlinear arithmetic over the reals: a new decision procedure for the existential theory of the reals allows efficient solving of systems of non-linear arithmetic constraints. The applications of this algorithm are many, ranging from hybrid systems to virtual reality environments;
  • inductive invariants and fixedpoints: new methods for the calculation of fixedpoints, which are central to discovering the inductive invariants needed to prove programs correct. These advances are due to Nikolaj Bjorner, Leonardo de Moura, Ken McMillan, and Margus Veanes at MSR, and their colleagues and interns.

Biography
Tom is a Principal Researcher and Research Manager at Microsoft Research (Redmond), where he works
in the area of software engineering, having made contributions in program profiling, software model
checking, and empirical software engineering. He is a 2011 ACM Fellow.