| Publication | Date of Publication | Type |
|---|
| Verification of threshold-based distributed algorithms by decomposition to decidable logics | 2024-02-16 | Paper |
| Property directed self composition | 2024-02-16 | Paper |
| Inferring inductive invariants from phase structures | 2024-02-16 | Paper |
| Modular verification of concurrent programs via sequential model checking | 2023-07-28 | Paper |
| Quantifiers on demand | 2023-07-28 | Paper |
| Invariant inference with provable complexity from the monotone theory | 2023-07-28 | Paper |
| SAT-based invariant inference and its relation to concept learning | 2023-07-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5090915 | 2022-07-21 | Paper |
| Synthesis with abstract examples | 2022-07-01 | Paper |
| Temporal prophecy for proving temporal properties of infinite-state systems | 2021-12-08 | Paper |
| Run-time complexity bounds using squeezers | 2021-10-18 | Paper |
| Global guidance for local generalization in model checking | 2021-02-09 | Paper |
| Putting the squeeze on array programs: loop verification via inductive rank reduction | 2020-08-05 | Paper |
| Solving \(\mathrm{LIA}^\star\) using approximations | 2020-08-05 | Paper |
| Bounded Quantifier Instantiation for Checking Inductive Invariants | 2020-08-05 | Paper |
| Abstraction-Based Interaction Model for Synthesis | 2020-07-07 | Paper |
| Programming by predicates: a formal model for interactive synthesis | 2020-03-06 | Paper |
| Automated Circular Assume-Guarantee Reasoning | 2019-12-19 | Paper |
| Some complexity results for stateful network verification | 2019-11-18 | Paper |
| Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs | 2019-09-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5232900 | 2019-09-13 | Paper |
| Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement | 2019-05-03 | Paper |
| Automated circular assume-guarantee reasoning | 2018-09-12 | Paper |
| Property-Directed Inference of Universal Invariants or Proving Their Absence | 2018-08-02 | Paper |
| Property-directed inference of universal invariants or proving their absence | 2018-03-01 | Paper |
| A game-based framework for CTL counterexamples and 3-valued abstraction-refinement | 2017-07-12 | Paper |
| Property Directed Reachability for Proving Absence of Concurrent Modification Errors | 2017-02-21 | Paper |
| IC3 - Flipping the E in ICE | 2017-02-21 | Paper |
| Decidability of inferring inductive invariants | 2016-10-24 | Paper |
| Decentralizing SDN Policies | 2016-09-29 | Paper |
| Symbolic automata for representing big code | 2016-06-28 | Paper |
| Property Directed Abstract Interpretation | 2016-03-23 | Paper |
| $$D^3$$ : Data-Driven Disjunctive Abstraction | 2016-03-23 | Paper |
| A framework for compositional verification of multi-valued systems via abstraction-refinement | 2016-03-10 | Paper |
| Symbolic Automata for Static Specification Mining | 2014-01-21 | Paper |
| Intertwined Forward-Backward Reachability Analysis Using Interpolants | 2013-08-05 | Paper |
| Multi-valued model checking games | 2012-05-11 | Paper |
| Computer Aided Verification | 2010-04-20 | Paper |
| Compositional verification and 3-valued abstractions join forces | 2010-02-26 | Paper |
| A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement | 2009-12-01 | Paper |
| Game semantics for the Lambek-calculus: Capturing directionality and the absence of structural rules | 2009-03-17 | Paper |
| Compositional Verification and 3-Valued Abstractions Join Forces | 2009-03-03 | Paper |
| 3-valued abstraction: More precision at less cost | 2008-12-03 | Paper |
| Tools and Algorithms for the Construction and Analysis of Systems | 2007-09-28 | Paper |
| When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus | 2007-08-23 | Paper |
| Automated Technology for Verification and Analysis | 2006-10-10 | Paper |
| Verification, Model Checking, and Abstract Interpretation | 2005-12-06 | Paper |
