| Publication | Date of Publication | Type |
|---|
| 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 | 2024-02-16 | Paper |
| Invertibility conditions for floating-point formulas | 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 | 2023-10-24 | Paper |
| Reasoning about vectors: satisfiability modulo a theory of sequences | 2023-10-24 | Paper |
| Synthesising programs with non-trivial constants | 2023-06-27 | Paper |
| Solving quantified bit-vectors using invertibility conditions | 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 | 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 | 2022-03-22 | Paper |
| Politeness and stable infiniteness: stronger together | 2021-12-01 | Paper |
| Towards satisfiability modulo parametric bit-vectors | 2021-11-24 | Paper |
| Syntax-guided quantifier instantiation | 2021-10-18 | Paper |
| On solving quantified bit-vector constraints using invertibility conditions | 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 | 2020-03-10 | Paper |
| Refutation-based synthesis in SMT | 2019-12-18 | Paper |
| A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method | 2019-10-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4553283 | 2018-11-02 | Paper |
| Datatypes with shared selectors | 2018-10-18 | Paper |
| Satisfiability Modulo Theories | 2018-07-20 | Paper |
| Counterexample-guided quantifier instantiation for synthesis in SMT | 2018-03-01 | Paper |
| Designing theory solvers with extensions | 2018-01-04 | Paper |
| Constraint solving for finite model finding in SMT solvers | 2017-11-09 | Paper |
| Relational constraint solving in SMT | 2017-09-22 | Paper |
| An efficient SMT solver for string constraints | 2017-03-28 | Paper |
| A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings | 2017-02-27 | Paper |
| A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT | 2016-09-05 | Paper |
| Model Finding for Recursive Functions in SMT | 2016-09-05 | Paper |
| Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors | 2016-01-12 | Paper |
| Solving SAT and SAT Modulo Theories | 2015-12-04 | Paper |
| SMT proof checking using a logical framework | 2014-03-28 | Paper |
| An abstract decision procedure for satisfiability in the theory of recursive data types | 2013-12-06 | Paper |
| Quantifier Instantiation Techniques for Finite Model Finding in SMT | 2013-06-14 | Paper |
| Combining Non-Stably Infinite Theories | 2013-04-19 | Paper |
| Model evolution with equality -- revised and implemented | 2012-06-20 | Paper |
| Ground interpolation for the theory of equality | 2012-04-03 | Paper |
| Model Evolution with Equality Modulo Built-in Theories | 2011-07-29 | Paper |
| Foundations of Satisfiability Modulo Theories | 2010-09-29 | Paper |
| Automated Deduction – CADE-19 | 2010-04-20 | Paper |
| Solving quantified verification conditions using satisfiability modulo theories | 2009-11-16 | Paper |
| Ground Interpolation for Combined Theories | 2009-07-28 | Paper |
| The model evolution calculus as a first-order DPLL method | 2009-07-17 | Paper |
| Ground Interpolation for the Theory of Equality | 2009-03-31 | Paper |
| Computing finite models by reduction to function-free clause logic | 2009-03-25 | Paper |
| Solving Quantified Verification Conditions Using Satisfiability Modulo Theories | 2009-03-06 | Paper |
| (LIA) - Model Evolution with Linear Integer Arithmetic Constraints | 2009-01-27 | Paper |
| Splitting on Demand in SAT Modulo Theories | 2008-05-27 | Paper |
| Lemma Learning in the Model Evolution Calculus | 2008-05-27 | Paper |
| An Abstract Framework for Satisfiability Modulo Theories | 2008-01-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5309032 | 2007-10-09 | Paper |
| Automated Reasoning | 2007-09-25 | Paper |
| Combined Satisfiability Modulo Parametric Theories | 2007-09-03 | Paper |
| Combining nonstably infinite theories | 2006-11-17 | Paper |
| Automated Deduction – CADE-20 | 2006-11-01 | Paper |
| Logics in Artificial Intelligence | 2006-10-25 | Paper |
| A new combination procedure for the word problem that generalizes fusion decidability results in modal logics | 2006-10-25 | Paper |
| Logic for Programming, Artificial Intelligence, and Reasoning | 2005-11-10 | Paper |
| Computer Aided Verification | 2005-08-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4808758 | 2004-08-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4708927 | 2003-06-20 | Paper |
| Cooperation of background reasoners in theory reasoning by residue sharing | 2003-06-09 | Paper |
| Unions of non-disjoint theories and combinations of satisfiability procedures | 2003-01-21 | Paper |
| Deciding the word problem in the union of equational theories. | 2002-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4518874 | 2000-12-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4938605 | 2000-02-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4259971 | 1999-09-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4385439 | 1998-07-20 | Paper |
