| Publication | Date of Publication | Type |
|---|
| An active learning approach to synthesizing program contracts | 2024-06-05 | Paper |
| A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification) | 2024-04-26 | Paper |
| On strings in software model checking | 2024-04-19 | Paper |
| Probabilistic bisimulation for parameterized systems (with applications to verifying anonymous protocols) | 2024-02-16 | Paper |
| OptiRica: towards an efficient optimizing Horn solver | 2024-02-16 | Paper |
| Automatic program instrumentation for automatic verification | 2024-02-01 | Paper |
| Decision procedures for sequence theories | 2024-01-12 | Paper |
| Regular model checking revisited | 2023-05-26 | Paper |
| A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type | 2022-12-22 | Paper |
| Monadic decomposition in integer linear arithmetic | 2022-11-09 | Paper |
| Reasoning in the theory of heap: satisfiability and interpolation | 2022-03-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5020662 | 2022-01-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5020659 | 2022-01-06 | Paper |
| Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic | 2021-12-08 | Paper |
| Horn clauses for communicating timed systems | 2021-06-28 | Paper |
| Characterization of simulation by probabilistic testing | 2021-05-20 | Paper |
| Fair termination for parameterized probabilistic concurrent systems | 2020-08-05 | Paper |
| Liveness of randomised parameterised systems under arbitrary schedulers | 2019-05-03 | Paper |
| Quantified Heap Invariants for Object-Oriented Programs | 2019-01-10 | Paper |
| Exploring approximations for floating-point arithmetic using UppSAT | 2018-10-18 | Paper |
| Automating regression verification of pointer programs by predicate abstraction | 2018-07-16 | Paper |
| An approximation framework for solvers and decision procedures | 2017-07-10 | Paper |
| Free variables and theories: revisiting rigid \(E\)-unification | 2017-02-27 | Paper |
| Deciding Bit-Vector Formulas with mcSAT | 2016-09-05 | Paper |
| Guiding Craig interpolation with domain-specific abstractions | 2016-06-28 | Paper |
| Regular symmetry patterns | 2016-03-23 | Paper |
| Efficient algorithms for bounded rigid \(E\)-unification | 2015-12-11 | Paper |
| Theorem proving with bounded rigid \(E\)-unification | 2015-12-02 | Paper |
| On recursion-free Horn clauses and Craig interpolation | 2015-10-20 | Paper |
| Approximations for Model Construction | 2014-09-26 | Paper |
| A theory for control-flow graph exploration | 2014-07-08 | Paper |
| Ranking function synthesis for bit-vector relations | 2014-06-30 | Paper |
| Ensuring the correctness of lightweight tactics for JavaCard dynamic logic | 2014-01-10 | Paper |
| Accelerating interpolants | 2012-11-21 | Paper |
| An interpolating sequent calculus for quantifier-free Presburger arithmetic | 2012-07-31 | Paper |
| E-matching with free variables | 2012-06-15 | Paper |
| Automatic analysis of DMA races using model checking and \(k\)-induction | 2012-03-09 | Paper |
| Beyond quantifier-free interpolation in extensions of Presburger arithmetic | 2011-02-15 | Paper |
| Mutation-Based Test Case Generation for Simulink Models | 2011-01-08 | Paper |
| Interpolating quantifier-free Presburger arithmetic | 2010-10-12 | Paper |
| An interpolating sequent calculus for quantifier-free Presburger arithmetic | 2010-09-14 | Paper |
| Ranking function synthesis for bit-vector relations | 2010-04-27 | Paper |
| A polymorphic intermediate verification language: design and logical encoding | 2010-04-27 | Paper |
| Real World Verification | 2009-07-28 | Paper |
| Integration of a Security Type System into a Program Logic | 2009-03-05 | Paper |
| A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic | 2009-01-27 | Paper |
| Integration of a security type system into a program logic | 2008-08-06 | Paper |
| Sequential, Parallel, and Quantified Updates of First-Order Structures | 2008-05-27 | Paper |
| Non-termination Checking for Imperative Programs | 2008-04-24 | Paper |
| Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic | 2007-10-31 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3021903 | 2005-06-21 | Paper |
