Date and Time: Thursday, 17 February 2011, 15:45 - 16:45

Location: HG 6.96

Speaker: Hans Zantema (TU/e / OAS)

Title: SAT solving, SMT solving and Program Verification

Abstract:

Where SAT solving is only about satisfiability of propositional formulas, SMT solving (Satisfiability Modulo Theories) is about richer theories, typically including linear (in)equalities over variables of type real or integer. In this talk some underlying ideas in current powerful SAT/SMT solvers are presented, and it is explained how this technology can be applied for program verification.