Talks

2023

  Local Search for Bit-Precise Reasoning and Beyond. October 3, 2023. Shonan Meeting No. 180: ‘The Art of SAT’, Shonan, Japan.
Slides

  IPASIR-UP: User Propagators for CDCL - A CaDiCaL Integration into CDCL(T). August 17, 2023. CENTAUR Annual Meeting 2023, Stanford, USA.
Slides Paper

  IPASIR-UP: User Propagators for CDCL. July 5, 2023. Satisfiability Modulo Theories (SMT) 2023, Rome, Italy.
Slides Paper

2022

  Local Search for Bit-Precise Reasoning and Beyond. August 11, 2022. Invited talk at Satisfiability Modulo Theories (SMT) 2022, Haifa, Israel.
Slides

  Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. August 8, 2022. Computer Aided Verification (CAV) 2022, Haifa, Israel.
Slides Paper

  Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. July 13, 2022. Centaur Annual Meeting, Stanford.
Slides Paper

  Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. March 2, 2022. AHA Affiliates Meeting, Stanford.
Slides Paper

2020

  Ternary Propagation-Based Local Search for more Bit-Precise Reasoning. September 24, 2020. Formal Methods in Computer-Aided Design (FMCAD) 2020, virtual.
Slides Video Paper

  Formal Checkers and Solvers for Hardware Design and Verification: Part 2 (SMT Solvers). July 30, 2020. Stanford Agile Hardware (AHA) Center (Virtual) Retreat 2020, virtual.
Slides

2019

  SMT-COMP 2019. July 8, 2017. 17th International Workshop on Satisfiability Modulo Theories (SMT) 2019, Lisbon, Portugal.
Slides

2018

  From Local Search to Quantifier-Elimination for Bit-Vectors in SMT. August 31, 2018. Banff International Research Station - Theory and Practice of Satisfiability Solving, Oaxaca, Mexico.
Slides

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

2017

  Model-Based API Testing for SMT Solvers. July 22, 2017. 15th International Workshop on Satisfiability Modulo Theories (SMT) 2017, Heidelberg, Germany.
Slides Paper Boolector

2016

  Precise and Complete Propagation-Based Local Search for Satisfiability Modulo Theories. July 20, 2016. 28th International Conference on Computer Aided Verification (CAV) 2016, Toronto, Ontario, Canada.
Slides Paper Boolector

2015

  Improving Local Search for Bit-Vector Logics with Path Propagation. October 26, 2015. International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS) 2015, Austin, Texas, USA.
Slides Paper Boolector

2014

  Turbo Charging Lemmas on Demand with Don’t Care Reasoning. October 23, 2014. Formal Methods in Computer-Aided Design (FMCAD) 2014, Lausanne, Switzerland.
Slides Paper Boolector

2013

  ddSMT: A Delta Debugger for the SMT-LIB v2 Format. July 8, 2017. 11th International Workshop on Satisfiability Modulo Theories (SMT) 2013, Helsinki, Finland.
Slides Paper ddSMT

2012

  Resolution-Based Certificate Extraction for QBF (Tool Presentation). July 17, 2012. 15th International Conference on Theory and Applications of Satisfiability Testing (SAT) 2012, Trento, Italy.
Slides Paper QBFcert