| Publication | Date of Publication | Type |
|---|
| https://portal.mardi4nfdi.de/entity/Q5874215 | 2023-02-07 | Paper |
| Display to Labeled Proofs and Back Again for Tense Logics | 2022-02-24 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5155663 | 2021-10-08 | Paper |
| An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model | 2021-06-09 | Paper |
| Compositional reasoning for shared-variable concurrent programs | 2021-05-04 | Paper |
| Quasi-Open Bisimilarity with Mismatch is Intuitionistic | 2021-01-20 | Paper |
| CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs | 2020-08-05 | Paper |
| Divergence and unique solution of equations | 2020-05-27 | Paper |
| Combining proverif and automated theorem provers for security protocol verification | 2020-03-10 | Paper |
| Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL | 2019-12-19 | Paper |
| De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic | 2019-11-22 | Paper |
| Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents | 2019-10-11 | Paper |
| Constructing weak simulations from linear implications for processes with private names | 2019-10-09 | Paper |
| Abella: A System for Reasoning about Relational Specifications | 2019-09-18 | Paper |
| A labelled sequent calculus for BBI: proof theory and proof search | 2019-01-31 | Paper |
| Modular Labelled Sequent Calculi for Abstract Separation Logics | 2018-08-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4608683 | 2018-03-21 | Paper |
| Semantics for Specialising Attack Trees based on Linear Logic | 2018-01-05 | Paper |
| Proof tactics for assertions in separation logic | 2018-01-04 | Paper |
| A proof theory for generic judgments | 2017-07-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2958523 | 2017-02-02 | Paper |
| Completeness for a First-Order Abstract Separation Logic | 2016-12-21 | Paper |
| On the role of names in reasoning about \(\lambda\)-tree syntax specifications | 2016-05-06 | Paper |
| Automated Theorem Proving for Assertions in Separation Logic with All Connectives | 2015-12-02 | Paper |
| Proof search specifications of bisimulation and modal logics for the π-calculus | 2015-09-17 | Paper |
| Extracting Proofs from Tabled Proof Search | 2015-01-13 | Paper |
| From Display Calculi to Deep Nested Sequent Calculi: Formalised for Full Intuitionistic Linear Logic | 2014-09-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5419898 | 2014-06-11 | Paper |
| Proof search for propositional abstract separation logics via labelled sequents | 2014-04-10 | Paper |
| A logic for reasoning about generic judgments | 2014-01-10 | Paper |
| Verification of clock synchronization algorithms: experiments on a combination of deductive tools | 2013-12-04 | Paper |
| A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search | 2013-10-04 | Paper |
| A proof search specification of the \(\pi\)-calculus | 2013-09-26 | Paper |
| Cut elimination for a logic with induction and co-induction | 2013-05-02 | Paper |
| Characterisations of testing preorders for a finite probabilistic \(\pi\)-calculus | 2013-03-22 | Paper |
| Stratification in Logics of Definitions | 2012-09-05 | Paper |
| Cut-elimination and proof search for bi-intuitionistic tense logic | 2012-08-05 | Paper |
| A Hypersequent System for Gödel-Dummett Logic with Non-constant Domains | 2011-07-01 | Paper |
| On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics | 2011-05-26 | Paper |
| A Local System for Classical Logic | 2011-05-06 | Paper |
| Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents | 2011-03-30 | Paper |
| A proof theoretic analysis of intruder theories | 2010-09-21 | Paper |
| Taming displayed tense logics using nested sequents with deep inference | 2009-12-01 | Paper |
| Formalising Observer Theory for Environment-Sensitive Bisimulation | 2009-10-20 | Paper |
| A First-Order Policy Language for History-Based Transaction Monitoring | 2009-08-20 | Paper |
| A Proof Theoretic Analysis of Intruder Theories | 2009-06-30 | Paper |
| Matching Trace Patterns with Regular Policies | 2009-04-02 | Paper |
| A Local System for Intuitionistic Logic | 2008-05-27 | Paper |
| A Trace Based Bisimulation for the Spi Calculus: An Extended Abstract | 2008-05-15 | Paper |
| Classical Modal Display Logic in the Calculus of Structures and Minimal Cut-free Deep Inference Calculi for S5 | 2007-11-19 | Paper |
| A System of Interaction and Structure II: The Need for Deep Inference | 2007-10-11 | Paper |
| Verification of clock synchronization algorithms: experiments on a combination of deductive tools | 2007-09-06 | Paper |
| Tools and Algorithms for the Construction and Analysis of Systems | 2007-05-02 | Paper |
| CONCUR 2005 – Concurrency Theory | 2006-11-01 | Paper |
| Types for Proofs and Programs | 2005-12-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4415240 | 2003-07-28 | Paper |
| Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents | N/A | Paper |
