Talks
2023
CaDiCaL(T): CaDiCaL as CDCL(T) Engine in cvc5.
October 3, 2022. Shonan Meeting 180: The Art of SAT, Shonan, Japan.Slides Bitwuzla.
July 20, 2022. 35th International Conference on Computer Aided Verification, Paris, France.Slides Paper 2022
Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers.
August 11, 2022. 20th International Workshop on Satisfiability Modulo Theories, Haifa, Israel.Slides Paper 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