| Publication | Date of Publication | Type |
|---|
| Stochastic games with lexicographic objectives | 2024-11-04 | Paper |
| Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate (Artifact) | 2024-10-11 | Dataset |
| Towards concurrent quantitative separation logic | 2024-08-13 | Paper |
| Parameter synthesis for Markov models: covering the parameter space | 2024-06-28 | Paper |
| Generative Datalog with continuous distributions | 2024-06-06 | Paper |
| Certificates for probabilistic pushdown automata via optimistic value iteration | 2024-04-05 | Paper |
| Probabilistic program verification via inductive synthesis of inductive invariants | 2024-04-05 | Paper |
| Formal Verification of Rewriting Rules for Dynamic Fault Trees | 2024-03-14 | Paper |
| Counterexample-driven synthesis for probabilistic program sketches | 2024-03-14 | Paper |
| Under-approximating expected total rewards in POMDPs | 2024-02-01 | Paper |
| Search and explore: symbiotic policy synthesis in POMDPs | 2024-02-01 | Paper |
| Model Checking Temporal Properties of Recursive Probabilistic Programs | 2024-01-23 | Paper |
| Model Checking Temporal Properties of Recursive Probabilistic Programs | 2024-01-16 | Paper |
| The probabilistic termination tool amber | 2024-01-08 | Paper |
| Shepherding hordes of Markov chains | 2023-11-24 | Paper |
| Automatically finding the right probabilities in Bayesian networks | 2023-10-23 | Paper |
| Convex Optimization for Parameter Synthesis in MDPs | 2023-09-26 | Paper |
| Parameter synthesis in Markov models: a gentle survey | 2023-08-10 | Paper |
| Foundations for entailment checking in quantitative separation logic | 2023-08-03 | Paper |
| Synthesis in pMDPs: a tale of 1001 parameters | 2023-07-28 | Paper |
| Rule-based conditioning of probabilistic data | 2023-07-28 | Paper |
| Markov automata with multiple objectives | 2023-06-29 | Paper |
| Model Checking for Safe Navigation Among Humans | 2023-06-28 | Paper |
| Parameter-Independent Strategies for pMDPs via POMDPs | 2023-06-28 | Paper |
| POMDP controllers with optimal budget | 2023-06-02 | Paper |
| Sound value iteration | 2023-05-26 | Paper |
| Monitoring CTMCs by multi-clock timed automata | 2023-05-26 | Paper |
| Causal ambiguity and partial orders in event structures | 2023-05-17 | Paper |
| Improving Generalization in Software IC3 | 2023-03-21 | Paper |
| Lower Bounds for Possibly Divergent Probabilistic Programs | 2023-02-12 | Paper |
| On the Complexity of Reachability in Parametric Markov Decision Processes | 2023-02-03 | Paper |
| Verification of Indefinite-Horizon POMDPs | 2022-12-22 | Paper |
| Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming | 2022-12-08 | Paper |
| Does a Program Yield the Right Distribution? | 2022-12-07 | Paper |
| Scenario-based verification of uncertain MDPs | 2022-10-13 | Paper |
| Simple strategies in multi-objective MDPs | 2022-10-13 | Paper |
| Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming | 2022-09-20 | Paper |
| Causal behaviours and nets | 2022-08-16 | Paper |
| Gradient-descent for randomized controllers under partial observability | 2022-07-08 | Paper |
| Out of control: reducing probabilistic models by control-state elimination | 2022-07-08 | Paper |
| Markov automata with multiple objectives | 2022-07-01 | Paper |
| Fine-tuning the odds in Bayesian networks | 2022-06-15 | Paper |
| Synthesizing optimal bias in randomized self-stabilization | 2022-04-01 | Paper |
| Synthesizing invariant barrier certificates via difference-of-convex programming | 2022-03-25 | Paper |
| Latticed \(k\)-induction with an application to probabilistic programs | 2022-03-25 | Paper |
| Tweaking the odds in probabilistic timed automata | 2022-03-24 | Paper |
| Generating functions for probabilistic programs | 2022-03-23 | Paper |
| The 10,000 facets of MDP model checking | 2022-02-16 | Paper |
| Bayesian inference by symbolic model checking | 2021-12-08 | Paper |
| Probabilistic model checking of AODV | 2021-12-08 | Paper |
| Automated termination analysis of polynomial probabilistic programs | 2021-10-18 | Paper |
| Counterexample-guided inductive synthesis for probabilistic systems | 2021-09-14 | Paper |
| Finding provably optimal Markov chains | 2021-08-04 | Paper |
| Inductive synthesis for probabilistic programs reaches new horizons | 2021-08-04 | Paper |
| Multi-objective optimization of long-run average and total rewards | 2021-08-04 | Paper |
| Strategy Synthesis for POMDPs in Robot Planning via Game-Based Abstractions | 2021-05-28 | Paper |
| The complexity of reachability in parametric Markov decision processes | 2021-04-14 | Paper |
| Expected Runtime Analyis by Program Verification | 2021-02-16 | Paper |
| \textsf{PrIC3}: property directed reachability for MDPs | 2021-02-09 | Paper |
| Stochastic games with lexicographic reachability-safety objectives | 2021-02-09 | Paper |
| A weakest pre-expectation semantics for mixed-sign expectations | 2021-01-19 | Paper |
| Design and analysis of dynamic leader election protocols in broadcast networks | 2020-11-30 | Paper |
| Multi-cost bounded tradeoff analysis in MDP | 2020-11-02 | Paper |
| Multi-objective Optimization of Long-run Average and Total Rewards: Supplemental Material | 2020-10-23 | Dataset |
| Sequential convex programming for the efficient verification of parametric MDPs | 2020-08-05 | Paper |
| Are parametric Markov chains monotonic? | 2020-07-20 | Paper |
| Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination | 2020-05-26 | Paper |
| Modal stochastic games. Abstraction-refinement of probabilistic automata | 2020-02-24 | Paper |
| One net fits all. A unifying semantics of dynamic fault trees using GSPNs | 2019-12-18 | Paper |
| Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems | 2019-09-17 | Paper |
| Multi-cost bounded reachability in MDP | 2019-09-16 | Paper |
| How long, O Bayesian network, will I sample thee? A program analysis perspective on expected sampling times | 2019-09-13 | Paper |
| On the hardness of analyzing probabilistic programs | 2019-03-21 | Paper |
| Weakest precondition reasoning for expected runtimes of randomized algorithms | 2019-02-25 | Paper |
| Parameter synthesis for Markov models: faster than ever | 2018-10-25 | Paper |
| Bounded model checking for probabilistic programs | 2018-10-25 | Paper |
| Model checking of open interval Markov chains | 2018-07-06 | Paper |
| On the satisfiability of some simple probabilistic logics | 2018-04-23 | Paper |
| Probably safe or live | 2018-04-23 | Paper |
| The probabilistic model checking landscape | 2018-04-23 | Paper |
| Reasoning about Recursive Probabilistic Programs | 2018-04-23 | Paper |
| Zero-reachability in probabilistic multi-counter automata | 2018-04-23 | Paper |
| Inferring covariances for probabilistic programs | 2018-01-11 | Paper |
| Fault trees on a diet: automated reduction by graph rewriting | 2017-09-08 | Paper |
| Fault trees on a diet -- automated reduction by graph rewriting | 2017-08-31 | Paper |
| Quantitative automata model checking of autonomous stochastic hybrid systems | 2017-05-16 | Paper |
| Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems | 2017-05-16 | Paper |
| Robust PCTL model checking | 2017-05-16 | Paper |
| Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components | 2017-03-28 | Paper |
| Quantitative model-checking of controlled discrete-time Markov processes | 2017-03-16 | Paper |
| Confluence reduction for Markov automata | 2017-02-06 | Paper |
| Conditioning in probabilistic programming | 2016-12-16 | Paper |
| Weakest precondition reasoning for expected run-times of probabilistic programs | 2016-04-26 | Paper |
| Probabilistic programming: a true verification challenge | 2016-01-08 | Paper |
| Fast debugging of PRISM models | 2015-12-17 | Paper |
| Weighted lumpability on Markov chains | 2015-12-07 | Paper |
| Understanding probabilistic programs | 2015-11-04 | Paper |
| Juggrnaut: using graph grammars for abstracting unbounded heap structures | 2015-10-20 | Paper |
| On the hardness of almost-sure termination | 2015-09-16 | Paper |
| Multi-objective parameter synthesis in probabilistic hybrid systems | 2015-09-14 | Paper |
| YMCA: why Markov chain algebra? | 2015-07-10 | Paper |
| Bisimulation and Simulation Relations for Markov Chains | 2015-07-10 | Paper |
| High-level counterexamples for probabilistic automata | 2015-04-22 | Paper |
| Counterexample generation for discrete-time Markov models: an introductory survey | 2015-02-25 | Paper |
| SMT-based bisimulation minimisation of Markov models | 2014-11-03 | Paper |
| Analysis of timed and long-run objectives for Markov automata | 2014-09-30 | Paper |
| Tight game abstractions of probabilistic automata | 2014-09-15 | Paper |
| Parametric LTL on Markov chains | 2014-09-15 | Paper |
| Minimal counterexamples for linear-time probabilistic verification | 2014-08-27 | Paper |
| A compositional modelling and analysis framework for stochastic hybrid systems | 2014-06-30 | Paper |
| Abstract probabilistic automata | 2013-12-13 | Paper |
| Model checking for performability | 2013-08-26 | Paper |
| A semantics for every GSPN | 2013-06-28 | Paper |
| Layered reasoning for randomized distributed algorithms | 2013-03-22 | Paper |
| Efficient modelling and generation of Markov automata | 2012-09-25 | Paper |
| Compositional abstraction techniques for probabilistic automata | 2012-09-21 | Paper |
| Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems | 2012-08-31 | Paper |
| Three-valued abstraction for probabilistic systems | 2012-08-14 | Paper |
| Minimal Critical Subsystems for Discrete-Time Markov Models | 2012-06-29 | Paper |
| A linear process-algebraic format with data for probabilistic automata | 2012-03-13 | Paper |
| Hierarchical counterexamples for discrete-time Markov chains | 2011-10-07 | Paper |
| Observing continuous-time MDPs by 1-clock timed automata | 2011-10-07 | Paper |
| A Local Greibach Normal Form for Hyperedge Replacement Grammars | 2011-06-03 | Paper |
| Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications | 2011-05-26 | Paper |
| Efficient CTMC Model Checking of Linear Real-Time Objectives | 2011-05-19 | Paper |
| A probabilistic extension of UML statecharts specification and verification | 2011-04-08 | Paper |
| Reachability in continuous-time Markov reward decision processes | 2011-03-30 | Paper |
| Approximate model checking of stochastic hybrid systems | 2011-03-09 | Paper |
| Abstract probabilistic automata | 2011-02-15 | Paper |
| The how and why of interactive Markov chains | 2011-01-08 | Paper |
| Linear-invariant generation for probabilistic programs: automated support for proof-based methods | 2010-10-01 | Paper |
| Performability assessment by model checking of Markov reward models | 2010-05-05 | Paper |
| CONCUR 2003 - Concurrency Theory | 2010-03-30 | Paper |
| Compositional abstraction for stochastic systems | 2009-12-01 | Paper |
| LTL model checking of time-inhomogeneous Markov chains | 2009-12-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5322945 | 2009-07-23 | Paper |
| Probabilistic weak simulation is decidable in polynomial time | 2009-07-09 | Paper |
| Delayed Nondeterminism in Continuous-Time Markov Decision Processes | 2009-03-31 | Paper |
| Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains | 2008-12-02 | Paper |
| Abstraction for Stochastic Systems by Erlang’s Method of Stages | 2008-11-25 | Paper |
| Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes | 2008-09-18 | Paper |
| Compositional Modeling and Minimization of Time-Inhomogeneous Markov Chains | 2008-09-02 | Paper |
| Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking | 2008-07-03 | Paper |
| Abstraction of Probabilistic Systems | 2008-07-03 | Paper |
| Three-Valued Abstraction for Continuous-Time Markov Chains | 2007-11-29 | Paper |
| Tools and Algorithms for the Construction and Analysis of Systems | 2007-09-28 | Paper |
| Safety and Liveness in Concurrent Pointer Programs | 2007-09-11 | Paper |
| Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking | 2007-09-03 | Paper |
| Counterexamples in Probabilistic Model Checking | 2007-09-03 | Paper |
| Model checking mobile stochastic logic | 2007-09-03 | Paper |
| Replaying Play In and Play Out: Synthesis of Design Models from Scenarios by Learning | 2007-09-03 | Paper |
| Formal Methods for the Design of Real-Time Systems | 2006-10-19 | Paper |
| Formal Modeling and Analysis of Timed Systems | 2006-01-10 | Paper |
| A theory of stochastic systems. II: Process algebra | 2005-12-07 | Paper |
| A theory of stochastic systems. I: Stochastic automata | 2005-12-07 | Paper |
| Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes | 2005-12-06 | Paper |
| Comparative branching-time semantics for Markov chains | 2005-09-02 | Paper |
| FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science | 2005-08-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4471933 | 2004-07-30 | Paper |
| Model-checking large structured Markov chains. | 2003-08-13 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4411090 | 2003-07-07 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4484497 | 2003-06-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4798036 | 2003-03-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4798032 | 2003-03-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4791266 | 2003-02-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4547773 | 2002-08-21 | Paper |
| Process algebra for performance evaluation | 2002-03-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2769589 | 2002-02-05 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2754096 | 2001-11-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2754196 | 2001-11-11 | Paper |
| Metric semantics for true concurrent real time | 2001-08-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4762660 | 2001-02-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4518904 | 2000-12-03 | Paper |
| Pattern-matching algorithms based on term rewrite systems | 2000-08-21 | Paper |
| Automated compositional Markov chain generation for a plain-old telephone system | 2000-07-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4270055 | 2000-04-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4255553 | 1999-08-17 | Paper |
| Systolic arrays for the recognition of permutation-invariant segments | 1997-03-31 | Paper |
| Code generation based on formal BURS theory and heuristic search | 1996-09-25 | Paper |
| Bottom-up tree acceptors | 1989-01-01 | Paper |
| Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains | N/A | Paper |
