| Publication | Date of Publication | Type |
|---|
| High-level abstractions for simplifying extended string constraints in SMT | 2024-02-16 | Paper |
| Invertibility conditions for floating-point formulas | 2024-02-16 | 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 |
| Satisfiability and synthesis modulo oracles | 2022-07-08 | 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 |
| Congruence closure with free variables | 2020-08-05 | 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 |
| Revisiting enumerative instantiation | 2019-09-16 | Paper |
| Reasoning with finite sets and cardinality constraints in SMT | 2018-11-02 | Paper |
| A decision procedure for separation logic in SMT | 2018-10-25 | Paper |
| Datatypes with shared selectors | 2018-10-18 | Paper |
| Deciding local theory extensions via E-matching | 2018-03-01 | Paper |
| Counterexample-guided quantifier instantiation for synthesis in SMT | 2018-03-01 | Paper |
| Solving quantified linear arithmetic by counterexample-guided instantiation | 2018-01-08 | 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 |
| A decision procedure for (co)datatypes in SMT solvers | 2017-06-29 | 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 |
| Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic | 2017-02-21 | 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 |
| A decision procedure for (co)datatypes in SMT solvers | 2015-12-02 | Paper |
| Induction for SMT solvers | 2015-02-04 | Paper |
| SMT proof checking using a logical framework | 2014-03-28 | Paper |
| Quantifier instantiation techniques for finite model finding in SMT | 2013-06-14 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4552140 | 2002-08-29 | Paper |
