Information
SAT and SMT solvers.
Held in MC 2038, on 2015-03-03, at 6:00 PM.
Abstract
Does your program have an overflow error? Will it work with all inputs? How
do you know for sure? Test cases are the bread and butter of resilient design,
but bugs still sneak into software. What if we could prove our programs are
error-free?
Boolean Satisfiability (SAT) solvers determine the ‘satisfiability’ of boolean
set of equations for a set of inputs. An SMT solver (Satisfiability Modulo
a Theory) applies SMT to bit-vectors, strings, arrays, and more. Together,
we can reduce a program and prove it is satisfiable, or provide a concrete
counter-example. The implications of this are computer-aided reasoning tools
for error-checking in addition to much more robust programs.
In this talk Murphy Berzish will give an overview of SAT/SMT theory and
some real-world solution methods. He will also demonstrate applications of
SAT/SMT solvers in theorem proving, model checking, and program verification.
What else? Oh yes, refreshments and drinks will be served. Come out!