| Publication | Date of Publication | Type |
|---|
| On the termination problem for probabilistic higher-order recursive programs | 2024-12-19 | Paper |
| An overview of the HFL model checking project | 2024-12-03 | Paper |
| Temporal verification of programs via first-order fixpoint logic | 2024-04-19 | Paper |
| A temporal logic for higher-order functional programs | 2024-04-19 | Paper |
| A type-based HFL model checking algorithm | 2024-04-19 | Paper |
| Neural network-guided synthesis of recursive list functions | 2023-12-13 | Paper |
| Gradual tensor shape checking | 2023-11-24 | Paper |
| https://portal.mardi4nfdi.de/entity/Q6176119 | 2023-08-21 | Paper |
| Automated synthesis of functional programs with auxiliary functions | 2023-08-02 | Paper |
| HoIce: an ICE-based non-linear Horn clause solver | 2023-08-02 | Paper |
| Parameterized recursive refinement types for automated program verification | 2023-07-28 | Paper |
| On higher-order reachability games vs may reachability | 2023-07-21 | Paper |
| Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination | 2023-03-29 | Paper |
| RustHorn: CHC-Based Verification for Rust Programs | 2022-10-13 | Paper |
| ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs | 2022-10-13 | Paper |
| Asynchronous unfold/fold transformation for fixpoint logic | 2022-08-10 | Paper |
| Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered | 2022-07-21 | Paper |
| Toward neural-network-guided program synthesis and verification | 2022-06-17 | Paper |
| Symbolic automatic relations and their applications to SMT and CHC solving | 2022-06-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5028436 | 2022-02-09 | Paper |
| Fold/Unfold Transformations for Fixpoint Logic | 2021-11-10 | Paper |
| Predicate abstraction and CEGAR for \(\nu \mathrm{HFL}_\mathbb{Z}\) validity checking | 2021-10-18 | Paper |
| A new refinement type system for automated \(\nu\text{HFL}_\mathbb{Z}\) validity checking | 2021-07-08 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5129945 | 2020-11-03 | Paper |
| ICE-based refinement type discovery for higher-order functional programs | 2020-11-02 | Paper |
| Pumping Lemma for Higher-order Languages | 2020-05-27 | Paper |
| Streett Automata Model Checking of Higher-Order Recursion Schemes | 2020-05-26 | Paper |
| ICE-based refinement type discovery for higher-order functional programs | 2019-09-16 | Paper |
| Higher-order program verification via HFL model checking | 2019-09-13 | Paper |
| Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable | 2019-06-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4625705 | 2019-02-25 | Paper |
| Equivalence-based abstraction refinement for \(\mu \)HORS model checking | 2018-10-25 | Paper |
| Automata-Based Abstraction Refinement for µHORS Model Checking | 2018-04-23 | Paper |
| Predicate abstraction and CEGAR for disproving termination of higher-order functional programs | 2018-03-01 | Paper |
| On word and frontier languages of unsafe higher-order grammars | 2017-12-19 | Paper |
| On the relationship between higher-order recursion schemes and higher-order fixpoint logic | 2017-10-20 | Paper |
| Pumping by Typing | 2017-07-03 | Paper |
| Modular Verification of Higher-Order Functional Programs | 2017-05-19 | Paper |
| Almost Every Simply Typed $$\lambda $$-Term Has a Long $$\beta $$-Reduction Sequence | 2017-05-19 | Paper |
| Functional programs as compressed data | 2017-05-15 | Paper |
| Automatically disproving fair termination of higher-order functional programs | 2017-05-10 | Paper |
| Compact bit encoding schemes for simply-typed lambda-terms | 2017-05-10 | Paper |
| Saturation-Based Model Checking of Higher-Order Recursion Schemes. | 2017-02-02 | Paper |
| Deadlock analysis of unbounded process networks | 2016-12-22 | Paper |
| Higher-Order Model Checking in Direct Style | 2016-12-21 | Paper |
| Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation | 2016-12-21 | Paper |
| Temporal verification of higher-order functional programs | 2016-10-24 | Paper |
| Verification of tree-processing programs via higher-order mode checking | 2016-07-27 | Paper |
| A ZDD-Based Efficient Higher-Order Model Checking Algorithm | 2016-02-26 | Paper |
| Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs | 2016-01-08 | Paper |
| Decision Algorithms for Checking Definability of Order-2 Finitary PCF | 2016-01-08 | Paper |
| Types and higher-order recursion schemes for verification of higher-order programs | 2015-07-03 | Paper |
| Higher-order multi-parameter tree transducers and recursion schemes for program verification | 2015-06-11 | Paper |
| A generic type system for the Pi-calculus | 2015-03-17 | Paper |
| Resource usage analysis | 2015-03-17 | Paper |
| Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes | 2015-01-12 | Paper |
| Automating relatively complete verification of higher-order functional programs | 2014-11-27 | Paper |
| Deadlock Analysis of Unbounded Process Networks | 2014-09-15 | Paper |
| Pairwise Reachability Analysis for Higher Order Concurrent Programs by Higher-Order Model Checking | 2014-09-15 | Paper |
| Complexity of Model-Checking Call-by-Value Programs | 2014-04-16 | Paper |
| Automatic Termination Verification for Higher-Order Functional Programs | 2014-04-16 | Paper |
| Unsafe Order-2 Tree Languages Are Context-Sensitive | 2014-04-16 | Paper |
| Model Checking Higher-Order Programs | 2014-02-17 | Paper |
| A Coq library for verification of concurrent programs | 2014-01-10 | Paper |
| Partial order reduction for verification of spatial properties of pi-calculus processes | 2013-09-25 | Paper |
| Model-Checking Higher-Order Programs with Recursive Types | 2013-08-05 | Paper |
| An Intersection Type System for Deterministic Pushdown Automata | 2012-09-21 | Paper |
| Exact Flow Analysis by Higher-Order Model Checking | 2012-07-20 | Paper |
| Type-based automated verification of authenticity in asymmetric cryptographic protocols | 2011-10-07 | Paper |
| A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes | 2011-05-19 | Paper |
| Untyped Recursion Schemes and Infinite Intersection Types | 2010-04-27 | Paper |
| Type systems for concurrent programs. | 2010-03-30 | Paper |
| Higher-order program verification and language-based security (extended abstract) | 2010-01-14 | Paper |
| Useless-code elimination and program slicing for the pi-calculus. | 2010-01-05 | Paper |
| Undecidable equivalences for basic parallel processes | 2009-07-15 | Paper |
| Type-Based Automated Verification of Authenticity in Cryptographic Protocols | 2009-03-31 | Paper |
| Extension of Type-Based Approach to Generation of Stream-Processing Programs by Automatic Insertion of Buffering Primitives | 2009-01-15 | Paper |
| A new type system for JVM lock primitives | 2008-10-20 | Paper |
| Tree Automata for Non-linear Arithmetic | 2008-08-28 | Paper |
| Maximum distributions of bridges of noncolliding Brownian paths | 2008-08-27 | Paper |
| Two Bessel bridges conditioned never to collide, double Dirichlet series, and Jacobi theta function | 2008-08-20 | Paper |
| A Hybrid Type System for Lock-Freedom of Mobile Processes | 2008-07-15 | Paper |
| Logical Bisimulations and Functional Languages | 2008-07-01 | Paper |
| Translation of tree-processing programs into stream-processing programs based on ordered linear type | 2008-05-22 | Paper |
| Type-Based Verification of Correspondence Assertions for Communication Protocols | 2008-05-15 | Paper |
| Substructural Type Systems for Program Analysis | 2008-04-11 | Paper |
| On-Demand Refinement of Dependent Types | 2008-04-11 | Paper |
| Linear Declassification | 2008-04-11 | Paper |
| Limit distributions of two-dimensional quantum walks | 2008-02-19 | Paper |
| Undecidability of 2-Label BPP Equivalences and Behavioral Type Systems for the π-Calculus | 2007-11-28 | Paper |
| Resource Usage Analysis for the Pi-Calculus | 2007-10-11 | Paper |
| A New Type System for Deadlock-Free Processes | 2007-09-04 | Paper |
| Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts | 2007-09-04 | Paper |
| Verification, Model Checking, and Abstract Interpretation | 2007-02-12 | Paper |
| A type system for lock-free processes | 2006-08-03 | Paper |
| Type-based information flow analysis for the \(\pi\)-calculus | 2006-01-10 | Paper |
| Programming Languages and Systems | 2005-08-17 | Paper |
| Programming Languages and Systems | 2005-08-17 | Paper |
| Dynamic Scaling of the Growing Rough Surfaces | 2005-03-21 | Paper |
| A generic type system for the pi-calculus | 2004-10-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4418577 | 2003-08-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4418578 | 2003-08-11 | Paper |
| Type reconstruction for linear \(\pi\)-calculus with I/O subtyping. | 2003-01-14 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4536437 | 2002-11-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4536623 | 2002-06-25 | Paper |
| Type-based useless-variable elimination | 2002-03-14 | Paper |
| A hybrid approach to online and offline partial evaluation | 2002-03-14 | Paper |
| Distributed concurrent linear logic programming | 2000-08-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4937839 | 2000-02-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4251120 | 1999-06-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4223021 | 1999-01-10 | Paper |
| Asynchronous communication model based on linear logic | 1995-09-25 | Paper |
