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

Speaker: Dr. Thomas Ball
         Microsoft Research (Redmond)

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

Date:    Monday, 26 November 2012

Time:    4:00pm - 5:00pm

Venue:   Lecture Theatre F (near lifts 25/26), HKUST

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.


********************
Biogarphy:

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.