Talks

2021

  Syntax-Guided Quantifier Instantiation. April 1, 2021. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’21), Virtual.
Slides Paper cvc5

2018

  Solving Quantified Bit-Vectors Using Invertibility Conditions. July 17, 2018. International Conference on Computer Aided Verification (CAV’18), Oxford, UK.
Slides Paper CVC4

  Practical SMT Session (SAT/SMT/AR Summer School 2018). July 4, 2018. SAT/SMT/AR Summer School 2018, Manchester, UK.
Slides

2017

  Counterexample-Guided Model Synthesis. July 22, 2017. International Workshop on Satisfiability Modulo Theories (SMT’17), Heidelberg, Germany.
Slides Paper Boolector

  Counterexample-Guided Model Synthesis. April 25, 2017. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’17), Uppsala, Sweden.
Slides Paper Boolector

2016

  Counterexample-Guided Model Synthesis for Quantified Bit-Vectors. November 18, 2016. Workshop on Automated Inductive Theorem-Proving (WAIT’16), Vienna, Austria.
Slides Paper Boolector

2015

  Better Lemmas with Lambda Extraction. September 29, 2015. Formal Methods in Computer-Aided Design (FMCAD) 2015, Austin, TX, USA.
Slides Paper Boolector

2013

  Lemmas on Demand for Lambdas. October 19, 2013. International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS’13), Portland, OR, USA.
Slides Paper Boolector

2012

  Scalable Certificate Extraction for QBF. May 22, 2012. Alpine Verification Meeting (AVM’12), Passau, Germany.
Slides Paper QBFcert