Advances in Automated Theorem Proving ... - DLS Talk by Thomas Ball, Microsoft Research
Date
–
Location
DMP 110, 6245 Agronomy Road
Speaker: Thomas Ball, Microsoft Research
Title: Advances in Automated Theorem Proving: Symbolic Automata, Nonlinear Arithmetic over the Reals, and Fixedpoint Calculation
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.
Event Series
DLS Schedule by Thomas Ball
Scheduling Contact
Associated Faculty