| Publication | Date of Publication | Type |
|---|
| Extended bounded response LTL: a new safety fragment for efficient reactive synthesis | 2025-01-13 | Paper |
| Expressiveness of extended bounded response \textsf{LTL} | 2024-12-06 | Paper |
| Invariant checking for SMT-based systems with quantifiers | 2024-11-12 | Paper |
| Efficient analysis of cyclic redundancy architectures via Boolean fault propagation | 2024-02-01 | Paper |
| A first-order logic characterisation of safety and co-safety languages | 2024-01-23 | Paper |
| Searching for ribbon-shaped paths in fair transition systems | 2024-01-23 | Paper |
| Searching for i-good lemmas to accelerate safety model checking | 2024-01-12 | Paper |
| Verification Modulo theories | 2023-10-30 | Paper |
| Efficient Anytime Computation and Execution of Decoupled Robustness Envelopes for Temporal Plans | 2023-10-02 | Paper |
| A first-order logic characterization of safety and co-safety languages | 2023-08-26 | Paper |
| SMT-based model checking of max-plus linear systems | 2023-08-21 | Paper |
| Verification of SMT systems with quantifiers | 2023-06-02 | Paper |
| Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test | 2023-06-02 | Paper |
| Fairness, assumptions, and guarantees for extended bounded response \textsf{LTL+P} synthesis | 2023-05-26 | Paper |
| Assumption-based runtime verification | 2023-05-08 | Paper |
| Analysis of cyclic fault propagation via ASP | 2023-04-04 | Paper |
| \textsc{LTL} falsification in infinite-state systems | 2022-12-08 | Paper |
| Abstraction Modulo Stability for Reverse Engineering | 2022-12-07 | Paper |
| \(\mathsf{GR}(1)\) is equivalent to \(\mathsf{R}(1)\) | 2022-10-28 | Paper |
| Safe Decomposition of Startup Requirements: Verification and Synthesis | 2022-10-13 | Paper |
| Diagnosability of fair transition systems | 2022-07-08 | Paper |
| Automatic discovery of fair paths in infinite-state transition systems | 2022-06-22 | Paper |
| Implicit semi-algebraic abstraction for polynomial dynamical systems | 2022-03-25 | Paper |
| Optimization modulo non-linear arithmetic via incremental linearization | 2022-03-24 | Paper |
| Universal invariant checking of parametric systems with quantifier-free SMT reasoning | 2021-12-01 | Paper |
| Proving the existence of fair paths in infinite-state systems | 2021-10-18 | Paper |
| Synthesis of P-stable abstractions | 2021-07-08 | Paper |
| Formal specification and verification of dynamic parametrized architectures | 2021-05-04 | Paper |
| Computation of the transient in max-plus linear systems via SMT-solving | 2021-03-02 | Paper |
| Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF | 2020-08-05 | Paper |
| SMT-based satisfiability of first-order LTL with event freezing functions and metric operators | 2020-05-26 | Paper |
| From electrical switched networks to hybrid automata | 2020-01-03 | Paper |
| Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations | 2019-05-03 | Paper |
| Mechanizing multi-agent reasoning with belief contexts | 2019-04-29 | Paper |
| Formal reliability analysis of redundancy architectures | 2019-03-13 | Paper |
| Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions | 2018-10-24 | Paper |
| Experimenting on solving nonlinear integer arithmetic with incremental linearization | 2018-08-10 | Paper |
| Tightening the contract refinements of a system architecture | 2018-08-08 | Paper |
| Satisfiability modulo transcendental functions via incremental linearization | 2017-09-22 | Paper |
| Infinite-state invariant checking with IC3 and predicate abstraction | 2017-07-26 | Paper |
| Satisfiability checking and symbolic computation | 2017-06-21 | Paper |
| Dynamic controllability via timed game automata | 2016-10-21 | Paper |
| $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation | 2016-08-30 | Paper |
| Formal Verification of Infinite-State BIP Models | 2016-01-08 | Paper |
| Formal Safety Assessment via Contract-Based Design | 2015-12-17 | Paper |
| HRELTL: a temporal logic for hybrid systems | 2015-12-07 | Paper |
| An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty | 2015-11-18 | Paper |
| Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic | 2015-11-05 | Paper |
| Efficient generation of craig interpolants in satisfiability modulo theories | 2015-09-17 | Paper |
| Solving strong controllability of temporal problems with uncertainty using SMT | 2015-04-29 | Paper |
| Quantifier-free encoding of invariants for hybrid systems | 2014-12-05 | Paper |
| SMT-based scenario verification for hybrid systems | 2014-03-28 | Paper |
| Encoding RTL constructs for \textsc{MathSAT}: a preliminary report | 2013-09-26 | Paper |
| Verifying industrial hybrid systems with \textsc{MathSAT} | 2013-09-20 | Paper |
| The MathSAT5 SMT Solver | 2013-08-05 | Paper |
| A Modular Approach to MaxSAT Modulo Theories | 2013-08-05 | Paper |
| Software model checking with explicit scheduler and symbolic threads | 2012-08-15 | Paper |
| Boosting Lazy Abstraction for SystemC with Partial Order Reduction | 2011-05-19 | Paper |
| Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories | 2011-05-04 | Paper |
| From Sequential Extended Regular Expressions to NFA with Symbolic Labels | 2011-02-11 | Paper |
| Satisfiability Modulo the Theory of Costs: Foundations and Applications | 2010-04-27 | Paper |
| Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis | 2009-11-16 | Paper |
| Interpolant Generation for UTVPI | 2009-07-28 | Paper |
| Requirements Validation for Hybrid Systems | 2009-06-30 | Paper |
| A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories | 2009-03-10 | Paper |
| Verifying Heap-Manipulating Programs in an SMT Framework | 2008-07-03 | Paper |
| Symbolic Fault Tree Analysis for Reactive Systems | 2008-07-03 | Paper |
| Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis | 2008-05-27 | Paper |
| To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in $\mathit{SMT}(\mathcal{EUF} \cup \mathcal{T})$ | 2008-05-27 | Paper |
| SYMBOLIC IMPLEMENTATION OF ALTERNATING AUTOMATA | 2008-05-20 | Paper |
| Efficient Interpolant Generation in Satisfiability Modulo Theories | 2008-04-11 | Paper |
| Diagnostic Information for Realizability | 2008-04-04 | Paper |
| Boolean Abstraction for Temporal Logic Satisfiability | 2007-11-29 | Paper |
| A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis | 2007-11-01 | Paper |
| Strong planning under partial observability | 2007-10-23 | Paper |
| Symbolic Implementation of Alternating Automata | 2007-09-06 | Paper |
| Formal Methods for Hardware Verification | 2007-05-02 | Paper |
| M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures | 2007-01-24 | Paper |
| Efficient theory combination via Boolean search | 2006-10-25 | Paper |
| Formal Methods in Computer-Aided Design | 2006-10-20 | Paper |
| Weak, strong, and strong cyclic planning via symbolic model checking | 2006-02-07 | Paper |
| Conformant planning via symbolic model checking and heuristic search | 2006-02-07 | Paper |
| Computer Aided Verification | 2006-01-10 | Paper |
| Tools and Algorithms for the Construction and Analysis of Systems | 2005-11-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4818818 | 2004-09-24 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4808722 | 2004-08-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4809056 | 2004-08-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4736997 | 2004-08-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4737124 | 2004-08-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4422082 | 2003-09-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4417910 | 2003-07-30 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4413373 | 2003-07-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4804909 | 2003-05-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4532080 | 2002-05-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2769595 | 2002-02-05 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4527271 | 2001-06-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4524503 | 2001-01-15 | Paper |
| NuSMV: A new symbolic model checker | 2000-01-01 | Paper |
| Computational reflection via mechanized logical deduction | 1997-01-13 | Paper |
