Seminars & Colloquia
"Advances in Automated Theorem Proving: Symbolic Automata, Nonlinear Arithmetic over the Reals, and Fixedpoint Calculation"
Monday March 25, 2013 04:00 PM
Location: 3211, EBII NCSU Centennial Campus
(Visitor parking instructions)
This talk is part of the Triangle Computer Science Distinguished Lecturer Series
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 Z3from Microsoft Research (MSR). In this talk, I’ll review advances from MSR that expand the scope of SMT solvers on several fronts.
These advances are due to Nikolaj Bjorner, Leonardo de Moura, Ken McMillan, and Margus Veanes at MSR, and their colleagues and interns.
Tomas Ball 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.
Host: Emerson Murphy-Hill, Computer Science, NCSU