Synthesis by Quantifier Instantiation in CVC4. Presented at AVM 2015.
Using CVC4 for Proofs by Induction. Presented at 2nd Workshop for Automated Inductive Theorem Proving, 2015.
Satisfiability Modulo Theories and DPLL(T). Presented at EPFL 2015.
Induction for SMT Solvers. Presented at VMCAI 2015.
Induction in CVC4. Presented at TU Munich 2014.
Finding Conflicting Instances of Quantified Formulas in SMT. Presented at FMCAD 2014.
A Tour of CVC4: How it Works, and how to Use it. Copresented with Morgan Deters and Tim King, FMCAD 2014.
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. Presented at CAV 2014.
Finding Conflicting Instances of Quantified Formulas in SMT. Presented at CEA Paris, 2014, QUANTIFY 2014.
A DPLL(T) Theory Solver for Strings and Regular Expressions. Presented at EPFL 2014.
Design of Theory Solvers in CVC4. Presented at EPFL 2014.
Finite Model Finding in Satisfiability Modulo Theories. Presented at University of Iowa, 2013.
Quantifier Instantiation Techniques for Finite Model Finding in SMT. Presented at CADE 24, 2013.
Model-Based Reasoning About Quantified Formulas in CVC4. Presented at University of Iowa, 2013, EPFL, 2013.
Extending SMT to Quantified Formulas. Presented at University of Iowa, 2012.
(Condensed Version) Generating Small Counterexamples Using SMT. Presented at MVD 2012, New York University 2012.
Generating Small Counterexamples Using SMT. Presented at Intel Research, 2012.
LFSC for SMT Proofs: Works in Process. Presented at PxTP, 2012.
Finite Model Finding for SMT. Presented at Intel and Microsoft Research, 2012.
Fast and Flexible Proof Checking with LFSC.. Presented at University of Iowa 2011.
A Counterexample-Based Approach for Quantifier Instantiation. Presented at New York University 2011, MVD 2011.
Certified Interpolant Generation for EUF. SMT 2011.
Comparing Proof Systems for Linear Real Arithmetic. Copresented with Liana Hadarean, SMT 2010. Also presented at MVD 2010.
Fast and Flexible Proof Checking for SMT. Copresented with Duckki Oe, SMT 2009 and MVD 2009.
I am the main developer of the module for handling quantified formulas in the SMT solver CVC4. It has been entered in the following competitions:
SMT Comp 2012
SMT Comp 2014