Talks
Satisfiability Modulo Theories solving: What, why and how
February 2023, Certora internal
Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver
August 2022, International Joint Conference on Automated Reasoning, Haifa, Israel
Cylindrical Algebraic Coverings for Quantifiers
August 2022, Satisfiability Checking and Symbolic Computation, Haifa, Israel
Satisfiability Modulo Theories for Arithmetic Problems
June 2022, Global Virtual SageDays, the world
Recent trends in SMT solving for nonlinear real arithmetic
March 2022, CSL Seminar, SRI International, Menlo Park, USA
Formal proofs for Cylindrical Algebraic Coverings
February 2022, New Perspectives in Symbolic Computation and Satisfiability Checking, Dagstuhl, Germany
On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving
December 2021, Symbolic and Numeric Algorithms for Scientific Computing, West University of Timisoara, Romania
Implementing arithmetic over algebraic numbers: A tutorial for Lazard's lifting scheme
December 2021, Symbolic and Numeric Algorithms for Scientific Computing, West University of Timisoara, Romania
Techniques for NRA in SMT
May 2021, Automated Reasoning in the Class, Training on SMT Solving
Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings
July 2020, International Congress on Mathematical Software, TU Braunschweig, Germany
Cylindrical Algebraic Decomposition for Nonlinear Arithmetic Problems
March 2020, RWTH Aachen University, Germany
On the proof complexity of MCSAT
July 2019, Satisfiability Checking and Symbolic Computation, Universität Bern, Switzerland
Incremental CAD
July 2018, International Congress on Mathematical Software, University of Notre Dame, USA
Computer Algebra and Computer Science
June 2018, Applications of Computer Algebra, University of Santiago de Compostela, Spain
Solving Pseudo-Boolean Constraints with SMT
March 2018, Siemens PLM Software, Leuven, Belgium
Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving
July 2017, Satisfiability Checking and Symbolic Computation, University of Kaiserslautern, Germany
Zephyrus2: On the Fly Deployment Optimization using SMT and CP Technologies
November 2016, Symposium on Dependable Software Engineering, Chinese Academy of Science, Beijing, China
Generalised Branch-and-Bound
September 2016, Computer Algebra in Scientific Computing in Bucharest, Romania
Recent trends in SMT solving
July 2016, Analytical Solutions and Reasoning group at University of Oslo, Norway
SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
November 2015, Symbolic Computation and Satisfiability Checking, Dagstuhl Seminar 15471, Dagstuhl, Germany
Using Cylindrical Algebraic Decomposition in Satisfiability Modulo Theories
June 2014, Joint Workshop of the German Research Training Groups in Computer Science, Dagstuhl, Germany
Satisfiability Modulo Real Arithmetic - SMT-Solving with CAD and Gröbner Bases
March 2014, Joint Workshop of Research Training Groups PUMA and AlgoSyn, Bonn, Germany