Talks
2026
Satisfiability Modulo Extensional Constant Arrays.
July 27, 2026. 38th International Conference on Computer Aided Verification, Lisbon, Portugal.Slides Paper Massively Parallel Bit-Precise Verification with Bitwuzla and Mallob.
April 16, 2026. 32nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Turin, Italy.Slides Paper 2024
Invited Talk: Challenges in Bit-Vector Reasoning.
July 23, 2024. 22nd International Workshop on Satisfiability Modulo Theories, Montreal, Canada.Slides 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