SAT and SMT solvers

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!