Sr. Research Scientist, Computer Science
Stanford University
353 Jane Stanford Way,
Stanford, CA, 94305, United States
CaDiCaL(T): CaDiCaL as CDCL(T) Engine in cvc5.
October 3, 2022. Shonan Meeting 180: The Art of SAT, Shonan, Japan.
Slides
Bitwuzla: A New SMT Solver For Bit-Precise Reasoning.
August 17, 2023. Centaur Annual Meeting, Stanford.
Slides
Bitwuzla.
July 20, 2022. 35th International Conference on Computer Aided Verification, Paris, France.
Slides Paper
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
cvc5: A Versatile and Industrial-Strength SMT Solver.
July 13, 2022. Centaur Annual Meeting, Stanford.
Slides cvc5
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
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
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
Counterexample-Guided Model Synthesis for Quantified Bit-Vectors.
November 18, 2016. Workshop on Automated Inductive Theorem-Proving (WAIT’16), Vienna, Austria.
Slides Paper Boolector
Better Lemmas with Lambda Extraction.
September 29, 2015. Formal Methods in Computer-Aided Design (FMCAD) 2015, Austin, TX, USA.
Slides Paper Boolector
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
Scalable Certificate Extraction for QBF.
May 22, 2012. Alpine Verification Meeting (AVM’12), Passau, Germany.
Slides Paper QBFcert