| Publication | Date of Publication | Type |
|---|
Search and explore: symbiotic policy synthesis in POMDPs
Formal Methods in System Design | 2026-03-23 | Paper |
| On certificates, expected runtimes, and termination in probabilistic pushdown automata | 2026-02-27 | Paper |
| A spectrum of approximate probabilistic bisimulations | 2026-02-10 | Paper |
Stochastic games with lexicographic objectives
Formal Methods in System Design | 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
Formal Methods in System Design | 2024-06-28 | Paper |
Generative Datalog with continuous distributions
Journal of the ACM | 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
Lecture Notes in Computer Science | 2024-01-23 | Paper |
Model checking temporal properties of recursive probabilistic programs
Logical Methods in Computer Science | 2024-01-16 | Paper |
The probabilistic termination tool amber
Formal Methods in System Design | 2024-01-08 | Paper |
Shepherding hordes of Markov chains
Tools and Algorithms for the Construction and Analysis of Systems | 2023-11-24 | Paper |
Automatically finding the right probabilities in Bayesian networks
The Journal of Artificial Intelligence Research (JAIR) | 2023-10-23 | Paper |
Convex Optimization for Parameter Synthesis in MDPs
IEEE Transactions on Automatic Control | 2023-09-26 | Paper |
Parameter synthesis in Markov models: a gentle survey
Lecture Notes in Computer Science | 2023-08-10 | Paper |
Foundations for entailment checking in quantitative separation logic
Programming Languages and Systems | 2023-08-03 | Paper |
Rule-based conditioning of probabilistic data
Lecture Notes in Computer Science | 2023-07-28 | Paper |
Synthesis in pMDPs: a tale of 1001 parameters
Automated Technology for Verification and Analysis | 2023-07-28 | Paper |
Markov automata with multiple objectives
Formal Methods in System Design | 2023-06-29 | Paper |
Parameter-Independent Strategies for pMDPs via POMDPs
Quantitative Evaluation of Systems | 2023-06-28 | Paper |
Model Checking for Safe Navigation Among Humans
Quantitative Evaluation of Systems | 2023-06-28 | Paper |
POMDP controllers with optimal budget
Quantitative Evaluation of Systems | 2023-06-02 | Paper |
Monitoring CTMCs by multi-clock timed automata
Computer Aided Verification | 2023-05-26 | Paper |
Sound value iteration
Computer Aided Verification | 2023-05-26 | Paper |
Causal ambiguity and partial orders in event structures
CONCUR '97: Concurrency Theory | 2023-05-17 | Paper |
Improving Generalization in Software IC3
Model Checking Software | 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
(available as arXiv preprint) | 2023-02-03 | Paper |
Verification of Indefinite-Horizon POMDPs
1517.68225 | 2022-12-22 | Paper |
Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming
Information and Computation | 2022-12-08 | Paper |
| Does a Program Yield the Right Distribution? | 2022-12-07 | Paper |
Simple strategies in multi-objective MDPs
Tools and Algorithms for the Construction and Analysis of Systems | 2022-10-13 | Paper |
Scenario-based verification of uncertain MDPs
Tools and Algorithms for the Construction and Analysis of Systems | 2022-10-13 | Paper |
Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming
(available as arXiv preprint) | 2022-09-20 | Paper |
Causal behaviours and nets
Lecture Notes in Computer Science | 2022-08-16 | Paper |
Gradient-descent for randomized controllers under partial observability
(available as arXiv preprint) | 2022-07-08 | Paper |
Out of control: reducing probabilistic models by control-state elimination
(available as arXiv preprint) | 2022-07-08 | Paper |
Markov automata with multiple objectives
Lecture Notes in Computer Science | 2022-07-01 | Paper |
Fine-tuning the odds in Bayesian networks
(available as arXiv preprint) | 2022-06-15 | Paper |
Synthesizing optimal bias in randomized self-stabilization
Distributed Computing | 2022-04-01 | Paper |
Synthesizing invariant barrier certificates via difference-of-convex programming
(available as arXiv preprint) | 2022-03-25 | Paper |
Latticed \(k\)-induction with an application to probabilistic programs
(available as arXiv preprint) | 2022-03-25 | Paper |
| Tweaking the odds in probabilistic timed automata | 2022-03-24 | Paper |
Generating functions for probabilistic programs
(available as arXiv preprint) | 2022-03-23 | Paper |
| The 10,000 facets of MDP model checking | 2022-02-16 | Paper |
Bayesian inference by symbolic model checking
(available as arXiv preprint) | 2021-12-08 | Paper |
| Probabilistic model checking of AODV | 2021-12-08 | Paper |
Automated termination analysis of polynomial probabilistic programs
(available as arXiv preprint) | 2021-10-18 | Paper |
Counterexample-guided inductive synthesis for probabilistic systems
Formal Aspects of Computing | 2021-09-14 | Paper |
Inductive synthesis for probabilistic programs reaches new horizons
(available as arXiv preprint) | 2021-08-04 | Paper |
Multi-objective optimization of long-run average and total rewards
(available as arXiv preprint) | 2021-08-04 | Paper |
| Finding provably optimal Markov chains | 2021-08-04 | Paper |
Strategy Synthesis for POMDPs in Robot Planning via Game-Based Abstractions
IEEE Transactions on Automatic Control | 2021-05-28 | Paper |
The complexity of reachability in parametric Markov decision processes
Journal of Computer and System Sciences | 2021-04-14 | Paper |
The complexity of reachability in parametric Markov decision processes
Journal of Computer and System Sciences | 2021-04-14 | Paper |
Expected Runtime Analyis by Program Verification
Foundations of Probabilistic Programming | 2021-02-16 | Paper |
Stochastic games with lexicographic reachability-safety objectives
(available as arXiv preprint) | 2021-02-09 | Paper |
\textsf{PrIC3}: property directed reachability for MDPs
(available as arXiv preprint) | 2021-02-09 | Paper |
| A weakest pre-expectation semantics for mixed-sign expectations | 2021-01-19 | Paper |
A weakest pre-expectation semantics for mixed-sign expectations
(available as arXiv preprint) | 2021-01-19 | Paper |
Design and analysis of dynamic leader election protocols in broadcast networks
Distributed Computing | 2020-11-30 | Paper |
Multi-cost bounded tradeoff analysis in MDP
Journal of Automated Reasoning | 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
Tools and Algorithms for the Construction and Analysis of Systems | 2020-08-05 | Paper |
Are parametric Markov chains monotonic?
Automated Technology for Verification and Analysis | 2020-07-20 | Paper |
Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination
Information and Computation | 2020-05-26 | Paper |
Modal stochastic games. Abstraction-refinement of probabilistic automata
Lecture Notes in Computer Science | 2020-02-24 | Paper |
One net fits all. A unifying semantics of dynamic fault trees using GSPNs
(available as arXiv preprint) | 2019-12-18 | Paper |
Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems
Information and Computation | 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
(available as arXiv preprint) | 2019-09-13 | Paper |
On the hardness of analyzing probabilistic programs
Acta Informatica | 2019-03-21 | Paper |
Weakest precondition reasoning for expected runtimes of randomized algorithms
Journal of the ACM | 2019-02-25 | Paper |
Parameter synthesis for Markov models: faster than ever
(available as arXiv preprint) | 2018-10-25 | Paper |
Bounded model checking for probabilistic programs
(available as arXiv preprint) | 2018-10-25 | Paper |
| Model checking of open interval Markov chains | 2018-07-06 | Paper |
Probably safe or live
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) | 2018-04-23 | Paper |
Probably safe or live
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) | 2018-04-23 | Paper |
The probabilistic model checking landscape
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science | 2018-04-23 | Paper |
Reasoning about Recursive Probabilistic Programs
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science | 2018-04-23 | Paper |
Zero-reachability in probabilistic multi-counter automata
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) | 2018-04-23 | Paper |
On the satisfiability of some simple probabilistic logics
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science | 2018-04-23 | Paper |
Inferring covariances for probabilistic programs
(available as arXiv preprint) | 2018-01-11 | Paper |
Fault trees on a diet: automated reduction by graph rewriting
Formal Aspects of Computing | 2017-09-08 | Paper |
Fault trees on a diet -- automated reduction by graph rewriting
Dependable Software Engineering: Theories, Tools, and Applications | 2017-08-31 | Paper |
Quantitative automata model checking of autonomous stochastic hybrid systems
Proceedings of the 14th international conference on Hybrid systems: computation and control | 2017-05-16 | Paper |
Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems
Proceedings of the 16th international conference on Hybrid systems: computation and control | 2017-05-16 | Paper |
Robust PCTL model checking
Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control | 2017-05-16 | Paper |
Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components
Formal Methods in System Design | 2017-03-28 | Paper |
Quantitative model-checking of controlled discrete-time Markov processes
Information and Computation | 2017-03-16 | Paper |
Confluence reduction for Markov automata
Theoretical Computer Science | 2017-02-06 | Paper |
Conditioning in probabilistic programming
Electronic Notes in Theoretical Computer Science | 2016-12-16 | Paper |
Weakest precondition reasoning for expected run-times of probabilistic programs
Programming Languages and Systems | 2016-04-26 | Paper |
Probabilistic programming: a true verification challenge
Automated Technology for Verification and Analysis | 2016-01-08 | Paper |
Fast debugging of PRISM models
Automated Technology for Verification and Analysis | 2015-12-17 | Paper |
Weighted lumpability on Markov chains
Perspectives of Systems Informatics | 2015-12-07 | Paper |
Understanding probabilistic programs
Lecture Notes in Computer Science | 2015-11-04 | Paper |
Juggrnaut: using graph grammars for abstracting unbounded heap structures
Formal Methods in System Design | 2015-10-20 | Paper |
On the hardness of almost-sure termination
Mathematical Foundations of Computer Science 2015 | 2015-09-16 | Paper |
Multi-objective parameter synthesis in probabilistic hybrid systems
Lecture Notes in Computer Science | 2015-09-14 | Paper |
YMCA: why Markov chain algebra?
Electronic Notes in Theoretical Computer Science | 2015-07-10 | Paper |
Bisimulation and Simulation Relations for Markov Chains
Electronic Notes in Theoretical Computer Science | 2015-07-10 | Paper |
High-level counterexamples for probabilistic automata
Logical Methods in Computer Science | 2015-04-22 | Paper |
Counterexample generation for discrete-time Markov models: an introductory survey
Lecture Notes in Computer Science | 2015-02-25 | Paper |
SMT-based bisimulation minimisation of Markov models
Lecture Notes in Computer Science | 2014-11-03 | Paper |
Analysis of timed and long-run objectives for Markov automata
Logical Methods in Computer Science | 2014-09-30 | Paper |
Tight game abstractions of probabilistic automata
CONCUR 2014 – Concurrency Theory | 2014-09-15 | Paper |
Parametric LTL on Markov chains
Advanced Information Systems Engineering | 2014-09-15 | Paper |
Minimal counterexamples for linear-time probabilistic verification
Theoretical Computer Science | 2014-08-27 | Paper |
A compositional modelling and analysis framework for stochastic hybrid systems
Formal Methods in System Design | 2014-06-30 | Paper |
Abstract probabilistic automata
Information and Computation | 2013-12-13 | Paper |
Model checking for performability
MSCS. Mathematical Structures in Computer Science | 2013-08-26 | Paper |
A semantics for every GSPN
Application and Theory of Petri Nets and Concurrency | 2013-06-28 | Paper |
Layered reasoning for randomized distributed algorithms
Formal Aspects of Computing | 2013-03-22 | Paper |
Efficient modelling and generation of Markov automata
Lecture Notes in Computer Science | 2012-09-25 | Paper |
Compositional abstraction techniques for probabilistic automata
Lecture Notes in Computer Science | 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
The Journal of Logic and Algebraic Programming | 2012-08-14 | Paper |
Minimal Critical Subsystems for Discrete-Time Markov Models
Tools and Algorithms for the Construction and Analysis of Systems | 2012-06-29 | Paper |
A linear process-algebraic format with data for probabilistic automata
Theoretical Computer Science | 2012-03-13 | Paper |
Observing continuous-time MDPs by 1-clock timed automata
Lecture Notes in Computer Science | 2011-10-07 | Paper |
Hierarchical counterexamples for discrete-time Markov chains
Automated Technology for Verification and Analysis | 2011-10-07 | Paper |
A Local Greibach Normal Form for Hyperedge Replacement Grammars
Language and Automata Theory and Applications | 2011-06-03 | Paper |
Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
Logical Methods in Computer Science | 2011-05-26 | Paper |
Efficient CTMC Model Checking of Linear Real-Time Objectives
Tools and Algorithms for the Construction and Analysis of Systems | 2011-05-19 | Paper |
A probabilistic extension of UML statecharts specification and verification
Lecture Notes in Computer Science | 2011-04-08 | Paper |
| Reachability in continuous-time Markov reward decision processes | 2011-03-30 | Paper |
Approximate model checking of stochastic hybrid systems
European Journal of Control | 2011-03-09 | Paper |
Abstract probabilistic automata
Lecture Notes in Computer Science | 2011-02-15 | Paper |
The how and why of interactive Markov chains
Formal Methods for Components and Objects | 2011-01-08 | Paper |
Linear-invariant generation for probabilistic programs: automated support for proof-based methods
Static Analysis | 2010-10-01 | Paper |
Performability assessment by model checking of Markov reward models
Formal Methods in System Design | 2010-05-05 | Paper |
CONCUR 2003 - Concurrency Theory
Lecture Notes in Computer Science | 2010-03-30 | Paper |
LTL model checking of time-inhomogeneous Markov chains
Automated Technology for Verification and Analysis | 2009-12-01 | Paper |
Compositional abstraction for stochastic systems
Lecture Notes in Computer Science | 2009-12-01 | Paper |
| scientific article; zbMATH DE number 5585443 (Why is no real title available?) | 2009-07-23 | Paper |
Probabilistic weak simulation is decidable in polynomial time
Information Processing Letters | 2009-07-09 | Paper |
Delayed Nondeterminism in Continuous-Time Markov Decision Processes
Foundations of Software Science and Computational Structures | 2009-03-31 | Paper |
Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains
Lecture Notes in Computer Science | 2008-12-02 | Paper |
Abstraction for Stochastic Systems by Erlang’s Method of Stages
CONCUR 2008 - Concurrency Theory | 2008-11-25 | Paper |
Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes
CONCUR 2007 – Concurrency Theory | 2008-09-18 | Paper |
Compositional Modeling and Minimization of Time-Inhomogeneous Markov Chains
Hybrid Systems: Computation and Control | 2008-09-02 | Paper |
Abstraction of Probabilistic Systems
Lecture Notes in Computer Science | 2008-07-03 | Paper |
Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking
Automated Technology for Verification and Analysis | 2008-07-03 | Paper |
Three-Valued Abstraction for Continuous-Time Markov Chains
Computer Aided Verification | 2007-11-29 | Paper |
Tools and Algorithms for the Construction and Analysis of Systems
Lecture Notes in Computer Science | 2007-09-28 | Paper |
Safety and Liveness in Concurrent Pointer Programs
Formal Methods for Components and Objects | 2007-09-11 | Paper |
Replaying Play In and Play Out: Synthesis of Design Models from Scenarios by Learning
Tools and Algorithms for the Construction and Analysis of Systems | 2007-09-03 | Paper |
Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking
Tools and Algorithms for the Construction and Analysis of Systems | 2007-09-03 | Paper |
Counterexamples in Probabilistic Model Checking
Tools and Algorithms for the Construction and Analysis of Systems | 2007-09-03 | Paper |
Model checking mobile stochastic logic
Theoretical Computer Science | 2007-09-03 | Paper |
Formal Methods for the Design of Real-Time Systems
Lecture Notes in Computer Science | 2006-10-19 | Paper |
Formal Modeling and Analysis of Timed Systems
Lecture Notes in Computer Science | 2006-01-10 | Paper |
A theory of stochastic systems. II: Process algebra
Information and Computation | 2005-12-07 | Paper |
A theory of stochastic systems. I: Stochastic automata
Information and Computation | 2005-12-07 | Paper |
Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
Theoretical Computer Science | 2005-12-06 | Paper |
Comparative branching-time semantics for Markov chains
Information and Computation | 2005-09-02 | Paper |
FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
Lecture Notes in Computer Science | 2005-08-12 | Paper |
| scientific article; zbMATH DE number 2079828 (Why is no real title available?) | 2004-07-30 | Paper |
Model-checking large structured Markov chains.
The Journal of Logic and Algebraic Programming | 2003-08-13 | Paper |
| scientific article; zbMATH DE number 1946767 (Why is no real title available?) | 2003-07-07 | Paper |
| scientific article; zbMATH DE number 1927572 (Why is no real title available?) | 2003-06-12 | Paper |
| scientific article; zbMATH DE number 1884414 (Why is no real title available?) | 2003-03-18 | Paper |
| scientific article; zbMATH DE number 1884412 (Why is no real title available?) | 2003-03-18 | Paper |
| scientific article; zbMATH DE number 1864588 (Why is no real title available?) | 2003-02-06 | Paper |
| scientific article; zbMATH DE number 1786481 (Why is no real title available?) | 2002-08-21 | Paper |
Process algebra for performance evaluation
Theoretical Computer Science | 2002-03-03 | Paper |
| scientific article; zbMATH DE number 1701761 (Why is no real title available?) | 2002-02-05 | Paper |
| scientific article; zbMATH DE number 1670788 (Why is no real title available?) | 2001-11-11 | Paper |
| scientific article; zbMATH DE number 1670870 (Why is no real title available?) | 2001-11-11 | Paper |
Metric semantics for true concurrent real time
Theoretical Computer Science | 2001-08-20 | Paper |
| scientific article; zbMATH DE number 1569132 (Why is no real title available?) | 2001-02-22 | Paper |
| scientific article; zbMATH DE number 1538048 (Why is no real title available?) | 2000-12-03 | Paper |
Pattern-matching algorithms based on term rewrite systems
Theoretical Computer Science | 2000-08-21 | Paper |
Automated compositional Markov chain generation for a plain-old telephone system
Science of Computer Programming | 2000-07-10 | Paper |
| scientific article; zbMATH DE number 1361121 (Why is no real title available?) | 2000-04-25 | Paper |
| scientific article; zbMATH DE number 1324654 (Why is no real title available?) | 1999-08-17 | Paper |
Systolic arrays for the recognition of permutation-invariant segments
Science of Computer Programming | 1997-03-31 | Paper |
Code generation based on formal BURS theory and heuristic search
Acta Informatica | 1996-09-25 | Paper |
Bottom-up tree acceptors
Science of Computer Programming | 1989-01-01 | Paper |
Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains
(available as arXiv preprint) | N/A | Paper |
