| Publication | Date of Publication | Type |
|---|
| Verifying SQL queries using theories of tables and relations | 2025-02-19 | Paper |
| An interactive SMT tactic in Coq using abductive reasoning | 2025-02-19 | Paper |
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 |
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 |
Satisfiability and synthesis modulo oracles
(available as arXiv preprint) | 2022-07-08 | 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 |
Congruence closure with free variables
Tools and Algorithms for the Construction and Analysis of Systems | 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
(available as arXiv preprint) | 2020-03-10 | Paper |
Refutation-based synthesis in SMT
Formal Methods in System Design | 2019-12-18 | Paper |
| Revisiting enumerative instantiation | 2019-09-16 | Paper |
Reasoning with finite sets and cardinality constraints in SMT
(available as arXiv preprint) | 2018-11-02 | Paper |
A decision procedure for separation logic in SMT
(available as arXiv preprint) | 2018-10-25 | Paper |
| Datatypes with shared selectors | 2018-10-18 | Paper |
Deciding local theory extensions via E-matching
(available as arXiv preprint) | 2018-03-01 | Paper |
Counterexample-guided quantifier instantiation for synthesis in SMT
(available as arXiv preprint) | 2018-03-01 | Paper |
Solving quantified linear arithmetic by counterexample-guided instantiation
Formal Methods in System Design | 2018-01-08 | 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 |
A decision procedure for (co)datatypes in SMT solvers
Journal of Automated Reasoning | 2017-06-29 | 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 |
Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
Lecture Notes in Computer Science | 2017-02-21 | 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 |
A decision procedure for (co)datatypes in SMT solvers
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
Induction for SMT solvers
Lecture Notes in Computer Science | 2015-02-04 | Paper |
SMT proof checking using a logical framework
Formal Methods in System Design | 2014-03-28 | Paper |
Quantifier instantiation techniques for finite model finding in SMT
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
| scientific article; zbMATH DE number 1792286 (Why is no real title available?) | 2002-08-29 | Paper |
