| Publication | Date of Publication | Type |
|---|
| Scalable proof production and checking in SMT (invited talk) | 2026-02-03 | Paper |
| SMT-LIB release 2024 (incremental benchmarks) | 2024-05-13 | Dataset |
| Formal Verification of Bit-Vector Invertibility Conditions in Coq | 2024-05-03 | Paper |
| SMT-LIB release 2024 (non-incremental benchmarks) | 2024-04-24 | Dataset |
High-level abstractions for simplifying extended string constraints in SMT
Computer Aided Verification | 2024-02-16 | Paper |
Invertibility conditions for floating-point formulas
Computer Aided Verification | 2024-02-16 | Paper |
| SMT-LIB release 2023 (incremental benchmarks) | 2024-02-01 | Dataset |
| SMT-LIB release 2023 (non-incremental benchmarks) | 2024-02-01 | Dataset |
| Satisfiability modulo finite fields | 2024-01-12 | Paper |
Combining stable infiniteness and (strong) politeness
Journal of Automated Reasoning | 2023-10-24 | Paper |
Reasoning about vectors: satisfiability modulo a theory of sequences
Journal of Automated Reasoning | 2023-10-24 | Paper |
Synthesising programs with non-trivial constants
Journal of Automated Reasoning | 2023-06-27 | Paper |
Solving quantified bit-vectors using invertibility conditions
Computer Aided Verification | 2023-05-05 | Paper |
| Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description) | 2022-12-07 | Paper |
| Even Faster Conflicts and Lazier Reductions for String Solvers | 2022-12-07 | Paper |
| Flexible proof production in an industrial-strength SMT solver | 2022-12-07 | Paper |
Reasoning about vectors using an SMT theory of sequences
(available as arXiv preprint) | 2022-12-07 | Paper |
| Scalable algorithms for abduction via enumerative syntax-guided synthesis | 2022-11-09 | Paper |
| A decision procedure for string to code point conversion | 2022-11-09 | Paper |
| SMTCoq: a plug-in for integrating SMT solvers into Coq | 2022-08-12 | Paper |
| Scaling up DPLL(T) string solvers using context-dependent simplification | 2022-08-12 | Paper |
Smt-Switch: a solver-agnostic C++ API for SMT solving
(available as arXiv preprint) | 2022-03-22 | Paper |
Politeness and stable infiniteness: stronger together
(available as arXiv preprint) | 2021-12-01 | Paper |
Towards satisfiability modulo parametric bit-vectors
Journal of Automated Reasoning | 2021-11-24 | Paper |
| Syntax-guided quantifier instantiation | 2021-10-18 | Paper |
On solving quantified bit-vector constraints using invertibility conditions
Formal Methods in System Design | 2021-08-30 | Paper |
| Theory combination: beyond equality sharing | 2020-06-04 | Paper |
| A tour of Franz Baader's contributions to knowledge representation and automated deduction | 2020-06-04 | Paper |
| Syntax-guided rewrite rule enumeration for SMT solvers | 2020-05-20 | Paper |
| Extending SMT solvers to higher-order logic | 2020-03-10 | Paper |
Towards bit-width-independent proofs in SMT solvers
(available as arXiv preprint) | 2020-03-10 | Paper |
Refutation-based synthesis in SMT
Formal Methods in System Design | 2019-12-18 | Paper |
A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
Automated Deduction—CADE-14 | 2019-10-01 | Paper |
Reasoning with finite sets and cardinality constraints in SMT
(available as arXiv preprint) | 2018-11-02 | Paper |
| Datatypes with shared selectors | 2018-10-18 | Paper |
Satisfiability modulo theories
Handbook of Model Checking | 2018-07-20 | Paper |
Counterexample-guided quantifier instantiation for synthesis in SMT
(available as arXiv preprint) | 2018-03-01 | Paper |
| Designing theory solvers with extensions | 2018-01-04 | Paper |
Constraint solving for finite model finding in SMT solvers
Theory and Practice of Logic Programming | 2017-11-09 | Paper |
| Relational constraint solving in SMT | 2017-09-22 | Paper |
An efficient SMT solver for string constraints
Formal Methods in System Design | 2017-03-28 | Paper |
A decision procedure for regular membership and length constraints over unbounded strings
Frontiers of Combining Systems | 2017-02-27 | Paper |
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
Automated Reasoning | 2016-09-05 | Paper |
Model finding for recursive functions in SMT
Automated Reasoning | 2016-09-05 | Paper |
Fine grained SMT proofs for the theory of fixed-width bit-vectors
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
Journal of the ACM | 2015-12-04 | Paper |
SMT proof checking using a logical framework
Formal Methods in System Design | 2014-03-28 | Paper |
An abstract decision procedure for satisfiability in the theory of recursive data types
Electronic Notes in Theoretical Computer Science | 2013-12-06 | Paper |
Quantifier instantiation techniques for finite model finding in SMT
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
Combining non-stably infinite theories
Electronic Notes in Theoretical Computer Science | 2013-04-19 | Paper |
Model evolution with equality -- revised and implemented
Journal of Symbolic Computation | 2012-06-20 | Paper |
Ground interpolation for the theory of equality
Logical Methods in Computer Science | 2012-04-03 | Paper |
Model Evolution with Equality Modulo Built-in Theories
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Foundations of satisfiability modulo theories
Logic, Language, Information and Computation | 2010-09-29 | Paper |
The model evolution calculus.
Lecture Notes in Computer Science | 2010-04-20 | Paper |
Solving quantified verification conditions using satisfiability modulo theories
Annals of Mathematics and Artificial Intelligence | 2009-11-16 | Paper |
Ground Interpolation for Combined Theories
Automated Deduction – CADE-22 | 2009-07-28 | Paper |
The model evolution calculus as a first-order DPLL method
Artificial Intelligence | 2009-07-17 | Paper |
Ground Interpolation for the Theory of Equality
Tools and Algorithms for the Construction and Analysis of Systems | 2009-03-31 | Paper |
Computing finite models by reduction to function-free clause logic
Journal of Applied Logic | 2009-03-25 | Paper |
Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
Automated Deduction – CADE-21 | 2009-03-06 | Paper |
(LIA) - Model Evolution with Linear Integer Arithmetic Constraints
Logic for Programming, Artificial Intelligence, and Reasoning | 2009-01-27 | Paper |
Splitting on Demand in SAT Modulo Theories
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
Lemma Learning in the Model Evolution Calculus
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
An Abstract Framework for Satisfiability Modulo Theories
Lecture Notes in Computer Science | 2008-01-04 | Paper |
| An abstract decision procedure for a theory of inductive data types. | 2007-10-09 | Paper |
Automated Reasoning
Lecture Notes in Computer Science | 2007-09-25 | Paper |
Combined Satisfiability Modulo Parametric Theories
Tools and Algorithms for the Construction and Analysis of Systems | 2007-09-03 | Paper |
Combining nonstably infinite theories
Journal of Automated Reasoning | 2006-11-17 | Paper |
Automated Deduction – CADE-20
Lecture Notes in Computer Science | 2006-11-01 | Paper |
Logics in Artificial Intelligence
Lecture Notes in Computer Science | 2006-10-25 | Paper |
A new combination procedure for the word problem that generalizes fusion decidability results in modal logics
Information and Computation | 2006-10-25 | Paper |
Logic for Programming, Artificial Intelligence, and Reasoning
Lecture Notes in Computer Science | 2005-11-10 | Paper |
Computer Aided Verification
Lecture Notes in Computer Science | 2005-08-25 | Paper |
| scientific article; zbMATH DE number 2090084 (Why is no real title available?) | 2004-08-12 | Paper |
| scientific article; zbMATH DE number 1931669 (Why is no real title available?) | 2003-06-20 | Paper |
Cooperation of background reasoners in theory reasoning by residue sharing
Journal of Automated Reasoning | 2003-06-09 | Paper |
Unions of non-disjoint theories and combinations of satisfiability procedures
Theoretical Computer Science | 2003-01-21 | Paper |
Deciding the word problem in the union of equational theories.
Information and Computation | 2002-01-01 | Paper |
| scientific article; zbMATH DE number 1538019 (Why is no real title available?) | 2000-12-03 | Paper |
| scientific article; zbMATH DE number 1405626 (Why is no real title available?) | 2000-02-23 | Paper |
| scientific article; zbMATH DE number 1332644 (Why is no real title available?) | 1999-09-09 | Paper |
| scientific article; zbMATH DE number 1140674 (Why is no real title available?) | 1998-07-20 | Paper |
