| Publication | Date of Publication | Type |
|---|
| Algebraic reasoning for (un)solvable loops (invited talk) | 2024-12-03 | Paper |
| Non-classical logics in satisfiability modulo theories | 2024-05-17 | Paper |
| SAT-Based Subsumption Resolution | 2024-04-26 | Paper |
| Program Synthesis in Saturation | 2024-04-26 | Paper |
| The probabilistic termination tool amber | 2024-01-08 | Paper |
| ALASCA: reasoning in quantified linear arithmetic | 2023-12-13 | Paper |
| Algebra-Based Loop Analysis | 2023-11-03 | Paper |
| From Polynomial Invariants to Linear Loops | 2023-11-03 | Paper |
| Algebra-Based Reasoning for Loop Synthesis | 2023-08-31 | Paper |
| Symbolic computation in automated program reasoning | 2023-08-17 | Paper |
| What else is undecidable about loops? | 2023-08-17 | Paper |
| Getting saturated with induction | 2023-08-10 | Paper |
| Solving invariant generation for unsolvable loops | 2023-07-28 | Paper |
| Distribution estimation for probabilistic loops | 2023-06-02 | Paper |
| Lemmaless induction in trace logic | 2023-06-02 | Paper |
| Algebra-Based Loop Synthesis | 2023-03-21 | Paper |
| Lonely points in simplices | 2023-01-23 | Paper |
| Subsumption demodulation in first-order theorem proving | 2022-11-09 | Paper |
| Inductive benchmarks for automated reasoning | 2022-04-22 | Paper |
| Automated generation of exam sheets for automated deduction | 2022-04-22 | Paper |
| Moment-based analysis of Bayesian network properties | 2022-02-01 | Paper |
| Integer induction in saturation | 2021-12-01 | Paper |
| Automated termination analysis of polynomial probabilistic programs | 2021-10-18 | Paper |
| Algebra-based synthesis of loops and their invariants (invited paper) | 2021-10-18 | Paper |
| Analysis of Bayesian networks via prob-solvable loops | 2021-07-08 | Paper |
| Induction with generalization in superposition reasoning | 2021-01-20 | Paper |
| Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences | 2020-09-09 | Paper |
| Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops | 2020-07-20 | Paper |
| Invariant Generation for Multi-Path Loops with Polynomial Assignments | 2020-07-07 | Paper |
| Loop Analysis by Quantification over Iterations | 2019-07-04 | Paper |
| First-Order Interpolation and Interpolating Proof Systems | 2019-01-10 | Paper |
| Aligator.jl -- a Julia package for loop invariant generation | 2018-10-18 | Paper |
| A FOOLish encoding of the next state relations of imperative programs | 2018-10-18 | Paper |
| Coming to terms with quantified reasoning | 2017-10-20 | Paper |
| Splitting proofs for interpolation | 2017-09-22 | Paper |
| Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution | 2017-02-06 | Paper |
| Segment Abstraction for Worst-Case Execution Time Analysis | 2016-04-26 | Paper |
| Reasoning About Loops Using Vampire in KeY | 2016-01-12 | Paper |
| Extensional Crisis and Proving Identity | 2015-12-17 | Paper |
| Symbolic Loop Bound Computation for WCET Analysis | 2015-12-07 | Paper |
| Lingva: Generating and Proving Program Properties Using Symbol Elimination | 2015-12-03 | Paper |
| A First Class Boolean Sort in First-Order Theorem Proving and TPTP | 2015-11-20 | Paper |
| Playing in the grey area of proofs | 2015-09-11 | Paper |
| Tree Interpolation in Vampire | 2014-01-17 | Paper |
| On Transfinite Knuth-Bendix Orders | 2011-07-29 | Paper |
| ABC: algebraic bound computation for loops | 2011-01-07 | Paper |
| Aligators for Arrays (Tool Paper) | 2010-10-12 | Paper |
| Solving the four fundamental problems from the theory of profile grids via BEM | 2010-09-17 | Paper |
| Deciding properties of affine loops | 2010-09-17 | Paper |
| Interpolation and symbol elimination in Vampire | 2010-09-14 | Paper |
| A complete invariant generation approach for P-solvable loops | 2010-02-02 | Paper |
| Invariant and type inference for matrices | 2010-01-14 | Paper |
| Interpolation and Symbol Elimination | 2009-07-28 | Paper |
| Valigator: A Verification Tool with Bound and Invariant Generation | 2009-01-27 | Paper |
| Aligator: A Mathematica Package for Invariant Generation (System Description) | 2008-11-27 | Paper |
| Invariant Generation for P-Solvable Loops with Assignments | 2008-06-05 | Paper |
| Reasoning Algebraically About P-Solvable Loops | 2008-04-11 | Paper |
| \textit{Theorema}: Towards computer-aided mathematical theory exploration | 2007-02-20 | Paper |
| Automated generation of loop invariants by recurrence solving in \texttt{Theorema} | 2007-01-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5699474 | 2005-10-26 | Paper |
| Linear Loop Synthesis for Quadratic Invariants | N/A | Paper |
