| Publication | Date of Publication | Type |
|---|
| Practical relational calculus query evaluation | 2024-04-25 | Paper |
| Practical relational calculus query evaluation | 2024-04-23 | Paper |
| Explainable online monitoring of metric temporal logic | 2024-04-05 | Paper |
| Verified first-order monitoring with recursive rules | 2024-02-01 | Paper |
| Efficient Evaluation of Arbitrary Relational Calculus Queries | 2024-01-16 | Paper |
| Optimal proofs for linear temporal logic on lasso words | 2023-07-28 | Paper |
| VeriMon: a formally verified monitoring tool | 2023-07-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q6157252 | 2023-06-20 | Paper |
| Generic Authenticated Data Structures, Formally. | 2023-02-03 | Paper |
| Multi-head Monitoring of Metric Dynamic Logic | 2022-12-22 | Paper |
| A formally verified, optimized monitor for metric first-order dynamic logic | 2022-11-09 | Paper |
| Quotients of Bounded Natural Functors | 2022-11-09 | Paper |
| From Nondeterministic to Multi-Head Deterministic Finite-State Transducers | 2022-07-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5028480 | 2022-02-09 | Paper |
| Distilling the requirements of Gödel's incompleteness theorems with a proof assistant | 2021-11-24 | Paper |
| Foundational nonuniform (co)datatypes for higher-order logic | 2021-01-19 | Paper |
| Formalizing Bachmair and Ganzinger's ordered resolution prover | 2020-11-02 | Paper |
| Almost event-rate independent monitoring of metric temporal logic | 2020-08-05 | Paper |
| Multi-head monitoring of metric temporal logic | 2020-07-20 | Paper |
| Adaptive online first-order monitoring | 2020-07-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5111307 | 2020-05-26 | Paper |
| A formally verified abstract account of Gödel's incompleteness theorems | 2020-03-10 | Paper |
| A survey of challenges for runtime verification from advanced application domains (beyond software) | 2019-11-25 | Paper |
| Almost event-rate independent monitoring | 2019-11-25 | Paper |
| Formalizing Bachmair and Ganzinger's ordered resolution prover | 2018-10-18 | Paper |
| Foundational (co)datatypes and (co)recursion for higher-order logic | 2018-01-04 | Paper |
| Verified decision procedures for MSO on words based on derivatives of regular expressions | 2017-10-23 | Paper |
| Formal Languages, Formally and Coinductively | 2017-10-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5367067 | 2017-10-12 | Paper |
| A coalgebraic decision procedure for WS1S | 2017-08-31 | Paper |
| Soundness and completeness proofs by coinductive methods | 2017-07-10 | Paper |
| Friends with benefits. Implementing corecursion in foundational proof assistants | 2017-05-19 | Paper |
| Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving | 2017-05-16 | Paper |
| Foundational extensible corecursion: a proof assistant perspective | 2017-05-10 | Paper |
| Witnessing (co)datatypes | 2016-04-26 | Paper |
| A formalized hierarchy of probabilistic system types. Proof pearl | 2015-09-14 | Paper |
| Verified decision procedures for MSO on words based on derivatives of regular expressions | 2015-03-30 | Paper |
| Unified Classical Logic Completeness | 2014-09-26 | Paper |
| Unified decision procedures for regular expression equivalence | 2014-09-08 | Paper |
| Truly modular (co)datatypes for Isabelle/HOL | 2014-09-08 | Paper |
| Cardinals in Isabelle/HOL | 2014-09-08 | Paper |
