| 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 |
| Global optimization of objective functions represented by ReLU networks | 2023-10-24 | Paper |
| Reasoning about vectors: satisfiability modulo a theory of sequences | 2023-10-24 | Paper |
| Combining stable infiniteness and (strong) politeness | 2023-10-24 | Paper |
| DeepSafe: a data-driven approach for assessing robustness of neural networks | 2023-07-28 | Paper |
| Reluplex: a calculus for reasoning about deep neural networks | 2023-06-29 | Paper |
| Synthesising programs with non-trivial constants | 2023-06-27 | Paper |
| Solving quantified bit-vectors using invertibility conditions | 2023-05-05 | Paper |
| Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness | 2023-05-03 | Paper |
| Verifying Recurrent Neural Networks Using Invariant Inference | 2022-12-22 | Paper |
| Flexible proof production in an industrial-strength SMT solver | 2022-12-07 | Paper |
| Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description) | 2022-12-07 | Paper |
| Reasoning about vectors using an SMT theory of sequences | 2022-12-07 | Paper |
| Even Faster Conflicts and Lazier Reductions for String Solvers | 2022-12-07 | Paper |
| A decision procedure for string to code point conversion | 2022-11-09 | Paper |
| Politeness for the theory of algebraic datatypes | 2022-11-09 | Paper |
| Polite combination of algebraic datatypes | 2022-10-24 | Paper |
| Partial Order Reduction for Deep Bug Finding in Synchronous Hardware | 2022-10-13 | Paper |
| Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays | 2022-10-06 | 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 |
| Reluplex: an efficient SMT solver for verifying deep neural networks | 2022-07-01 | 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 |
| An SMT-based approach for verifying binarized neural networks | 2021-10-18 | Paper |
| On solving quantified bit-vector constraints using invertibility conditions | 2021-08-30 | Paper |
| Counterexample-guided prophecy for model checking modulo the theory of arrays | 2021-08-04 | Paper |
| Syntax-guided rewrite rule enumeration for SMT solvers | 2020-05-20 | Paper |
| DRAT-based bit-vector proofs in CVC4 | 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 |
| https://portal.mardi4nfdi.de/entity/Q5219923 | 2020-03-09 | Paper |
| Refutation-based synthesis in SMT | 2019-12-18 | 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 |
| Deciding local theory extensions via E-matching | 2018-03-01 | 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 |
| Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors | 2016-01-12 | Paper |
| Book review of: Daniel Kroening and Ofer Strichman, Decision procedures: an algorithmic point of view | 2015-06-23 | Paper |
| Being careful about theory combination | 2014-03-28 | Paper |
| An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types | 2013-12-06 | Paper |
| Witness Runs for Counter Machines | 2013-10-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2848688 | 2013-09-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2848051 | 2013-09-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2848053 | 2013-09-25 | Paper |
| Witness Runs for Counter Machines | 2013-09-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2844808 | 2013-08-19 | Paper |
| Quantifier Instantiation Techniques for Finite Model Finding in SMT | 2013-06-14 | Paper |
| Sharing Is Caring: Combination of Theories | 2011-10-07 | Paper |
| Polite Theories Revisited | 2010-10-12 | Paper |
| Solving quantified verification conditions using satisfiability modulo theories | 2009-11-16 | Paper |
| Solving Quantified Verification Conditions Using Satisfiability Modulo Theories | 2009-03-06 | Paper |
| Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors | 2008-08-28 | Paper |
| Splitting on Demand in SAT Modulo Theories | 2008-05-27 | Paper |
| Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006) | 2007-11-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5309032 | 2007-10-09 | Paper |
| Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005) | 2007-01-30 | Paper |
| Translation and run-time validation of loop transformations | 2006-01-23 | Paper |
| Computer Aided Verification | 2006-01-10 | Paper |
| Computer Aided Verification | 2006-01-10 | Paper |
| Computer Aided Verification | 2005-08-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4737130 | 2004-08-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4804899 | 2003-05-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4804919 | 2003-05-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2723410 | 2001-07-05 | Paper |
