| Publication | Date of Publication | Type |
|---|
| LISA -- a modern proof system | 2024-11-26 | Paper |
| Succinct ordering and aggregation constraints in algebraic array theories | 2024-06-25 | Paper |
| On algebraic array theories | 2024-02-12 | Paper |
| Equivalence checking for orthocomplemented bisemilattices in log-linear time | 2024-02-01 | Paper |
| Formula normalizations in verification | 2024-02-01 | Paper |
| Orthologic with Axioms | 2023-07-14 | Paper |
| NP satisfiability for arrays as powers | 2022-07-08 | Paper |
| Generalized arrays for Stainless frames | 2022-07-08 | Paper |
| Minimal synthesis of string to string functions from examples | 2020-01-23 | Paper |
| Refutation-based synthesis in SMT | 2019-12-18 | 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 |
| Contract-based resource verification for higher-order functions with memoization | 2017-10-20 | Paper |
| Translating Scala Programs to Isabelle/HOL | 2016-09-05 | Paper |
| On recursion-free Horn clauses and Craig interpolation | 2015-10-20 | Paper |
| Decision procedures for algebraic data types with abstractions | 2015-06-11 | Paper |
| Role analysis | 2015-03-17 | Paper |
| Induction for SMT Solvers | 2015-02-04 | Paper |
| Reductions for Synthesis Procedures | 2014-11-03 | Paper |
| Verifying and Synthesizing Software with Recursive Functions | 2014-07-01 | Paper |
| Sound compilation of reals | 2014-04-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4924969 | 2013-06-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4922308 | 2013-05-29 | Paper |
| Accelerating Interpolants | 2012-11-21 | Paper |
| Synthesis for Unbounded Bit-Vector Arithmetic | 2012-09-05 | Paper |
| An Efficient Decision Procedure for Imperative Tree Data Structures | 2011-07-29 | Paper |
| Scala to the Power of Z3: Integrating SMT and Programming | 2011-07-29 | Paper |
| Towards Complete Reasoning about Axiomatic Specifications | 2011-02-15 | Paper |
| Sets with Cardinality Constraints in Satisfiability Modulo Theories | 2011-02-15 | Paper |
| MUNCH - Automated Reasoner for Sets and Multisets | 2010-09-14 | Paper |
| Ordered Sets in the Calculus of Data Structures | 2010-09-03 | Paper |
| Building a Calculus of Data Structures | 2010-01-14 | Paper |
| Collections, Cardinalities, and Relations | 2010-01-14 | Paper |
| Combining Theories with Shared Set Operations | 2010-01-07 | Paper |
| Verification, Model Checking, and Abstract Interpretation | 2009-05-15 | Paper |
| Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic | 2009-03-06 | Paper |
| Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars | 2008-11-20 | Paper |
| Linear Arithmetic with Stars | 2008-07-15 | Paper |
| Using First-Order Theorem Provers in the Jahob Data Structure Verification System | 2008-04-04 | Paper |
| Decision Procedures for Multisets with Cardinality Constraints | 2008-04-04 | Paper |
| Runtime Checking for Separation Logic | 2008-04-04 | Paper |
| Polynomial Constraints for Sets with Cardinality Bounds | 2007-09-07 | Paper |
| Verification, Model Checking, and Abstract Interpretation | 2007-02-12 | Paper |
| Deciding Boolean algebra with Presburger arithmetic | 2007-01-30 | Paper |
| Automated Deduction – CADE-20 | 2006-11-01 | Paper |
| Verification, Model Checking, and Abstract Interpretation | 2005-12-06 | Paper |
| Static Analysis | 2005-08-24 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4813414 | 2004-08-13 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4448356 | 2004-02-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4424843 | 2003-09-07 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4794072 | 2003-02-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3148997 | 2002-09-24 | Paper |
