| Publication | Date of Publication | Type |
|---|
| Analysis of core-guided maxsat using cores and correction sets | 2024-07-12 | Paper |
| On Incremental Pre-processing for SMT | 2024-04-26 | Paper |
| Algebra-Based Reasoning for Loop Synthesis | 2023-08-31 | Paper |
| Algebra-Based Loop Synthesis | 2023-03-21 | Paper |
| Supercharging plant configurations using Z3 | 2022-03-21 | Paper |
| Solving \(\mathrm{LIA}^\star\) using approximations | 2020-08-05 | Paper |
| Guiding high-performance SAT solvers with unsat-core predictions | 2020-05-20 | Paper |
| A practical integration of first-order reasoning and decision procedures | 2019-10-01 | Paper |
| Constrained image generation using binarized neural networks with decision procedures | 2018-08-10 | Paper |
| Property-Directed Inference of Universal Invariants or Proving Their Absence | 2018-08-02 | Paper |
| Monadic Decomposition | 2018-05-17 | Paper |
| Property-directed inference of universal invariants or proving their absence | 2018-03-01 | Paper |
| Equivalence of Finite-Valued Symbolic Finite Transducers | 2016-12-21 | Paper |
| Scaling network verification using symmetry and surgery | 2016-10-24 | Paper |
| Symbolic Tree Transducers | 2015-12-07 | Paper |
| Horn Clause Solvers for Program Verification | 2015-09-22 | Paper |
| Symbolic finite state transducers | 2015-09-11 | Paper |
| Property Directed Polyhedral Abstraction | 2015-02-04 | Paper |
| Symbolic tree automata | 2014-12-15 | Paper |
| Computing All Implied Equalities via SMT-Based Partition Refinement | 2014-09-26 | Paper |
| Resourceful Reachability as HORN-LA | 2014-01-17 | Paper |
| Model-based theory combination | 2013-12-06 | Paper |
| Generalized Property Directed Reachability | 2013-08-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4904149 | 2013-01-28 | Paper |
| Taking Satisfiability to the Next Level with Z3 | 2012-09-05 | Paper |
| Canonical regular types | 2012-08-29 | Paper |
| From Primal Infon Logic with Individual Variables to Datalog | 2012-07-23 | Paper |
| Symbolic Automata: The Toolkit | 2012-06-29 | Paper |
| Symbolic Automata Constraint Solving | 2010-10-12 | Paper |
| Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development | 2010-09-14 | Paper |
| Linear Quantifier Elimination as an Abstract Decision Procedure | 2010-09-14 | Paper |
| DKAL and Z3: A Logic Embedding Experiment | 2010-09-03 | Paper |
| Deciding effectively propositional logic using DPLL and substitution sets | 2010-05-26 | Paper |
| Content-dependent chunking for differential compression, the local maximum approach | 2010-05-25 | Paper |
| Symbolic Bounded Conformance Checking of Model Programs | 2010-02-02 | Paper |
| Satisfiability Modulo Theories: An Appetizer | 2009-12-09 | Paper |
| Input-Output Model Programs | 2009-08-20 | Paper |
| Linear Functional Fixed-points | 2009-06-30 | Paper |
| Path Feasibility Analysis for String-Manipulating Programs | 2009-03-31 | Paper |
| Efficient E-Matching for SMT Solvers | 2009-03-06 | Paper |
| Deciding Effectively Propositional Logic Using DPLL and Substitution Sets | 2008-11-27 | Paper |
| Engineering DPLL(T) + Saturation | 2008-11-27 | Paper |
| Models and Software Model Checking of a Distributed File Replication System | 2008-09-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2723889 | 2001-07-08 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4952308 | 2001-03-12 | Paper |
| Deductive verification of real-time systems using STeP | 2000-12-12 | Paper |
| Automatic generation of invariants and intermediate assertions | 1998-07-23 | Paper |
