Personal tools
You are here: Home Events Lab lunch speakers 2010 Grant Passmore

Grant Passmore

I'll present at a high level some recent joint work by myself and Leonoardo de Moura (Microsoft Research, Redmond) on extending SMT (`SAT modulo theories') solvers with support for nonlinear real arithmetic. This includes work on novel Gr\"obner basis construction algorithms tailored to the needs of SMT solvers, as well as techniques for minimising complex nullstellensatz proofs (so as to obtain `unsat cores' which are important for efficient SMT solving). These techniques have been implemented by de Moura in the latest incarnation of his Z3 SMT solver

Document Actions