| Publication | Date of Publication | Type |
|---|
| A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL | 2024-02-06 | Paper |
| A strict constrained superposition calculus for graphs | 2023-11-24 | Paper |
| A proof procedure for separation logic with inductive definitions and data | 2023-10-24 | Paper |
| Unbiasing and robustifying implied volatility calibration in a cryptocurrency market with large bid-ask spreads and missing quotes | 2023-09-25 | Paper |
| An undecidability result for separation logic with theory reasoning | 2023-06-05 | Paper |
| Unifying decidable entailments in separation logic with inductive definitions | 2021-12-01 | Paper |
| Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules | 2021-10-19 | Paper |
| The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates | 2020-09-11 | Paper |
| Prenex separation logic with one selector field | 2020-05-14 | Paper |
| Ilinva: using abduction to generate loop invariants | 2020-05-13 | Paper |
| Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL | 2020-04-07 | Paper |
| Combining induction and saturation-based theorem proving | 2020-03-03 | Paper |
| The Bernays-Schönfinkel-Ramsey class of separation logic on arbitrary domains | 2020-01-28 | Paper |
| A generic framework for implicate generation modulo theories | 2018-10-18 | Paper |
| Prime Implicate Generation in Equational Logic | 2018-01-12 | Paper |
| The binomial pricing model in finance: a formalization in Isabelle | 2017-09-22 | Paper |
| A superposition calculus for abductive reasoning | 2017-08-17 | Paper |
| Quantifier-Free Equational Logic and Prime Implicate Generation | 2015-12-02 | Paper |
| Instantiation Schemes for Nested Theories | 2015-09-17 | Paper |
| A Rewriting Strategy to Generate Prime Implicates in Equational Logic | 2014-09-26 | Paper |
| Rewrite-Based Decision Procedures | 2013-12-06 | Paper |
| Rewrite-Based Satisfiability Procedures for Recursive Data Structures | 2013-12-06 | Paper |
| A Resolution Calculus for First-order Schemata | 2013-08-26 | Paper |
| On leaf permutative theories and occurrence permutation groups | 2013-04-19 | Paper |
| Modular instantiation schemes | 2013-04-04 | Paper |
| Reasoning on Schemata of Formulæ | 2012-09-07 | Paper |
| A Calculus for Generating Ground Explanations | 2012-09-05 | Paper |
| An instantiation scheme for satisfiability modulo theories | 2012-07-31 | Paper |
| Instantiation of SMT Problems Modulo Integers | 2010-08-24 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3408147 | 2010-02-24 | Paper |
| Theory decision by decomposition | 2009-12-03 | Paper |
| ${\mathcal{T}}$ -Decision by Decomposition | 2009-03-06 | Paper |
| Unification and Matching Modulo Leaf-Permutative Equational Presentations | 2008-11-27 | Paper |
| On Variable-inactivity and Polynomial Formula-Satisfiability Procedures | 2008-03-12 | Paper |
| Determining Unify-Stable Presentations | 2008-01-02 | Paper |
| Automated Reasoning | 2007-09-25 | Paper |
| Permutative rewriting and unification | 2007-04-16 | Paper |
| Term Rewriting and Applications | 2005-11-11 | Paper |
| On the complexity of deduction modulo leaf permutative equations | 2005-06-22 | Paper |
