research
∙
09/14/2023
A Deductive Verification Infrastructure for Probabilistic Programs
This paper presents a quantitative program verification infrastructure f...
share
research
∙
07/14/2023
Exact Bayesian Inference for Loopy Probabilistic Programs
We present an exact Bayesian inference method for inferring posterior di...
research
∙
05/23/2023
Search and Explore: Symbiotic Policy Synthesis in POMDPs
This paper marries two state-of-the-art controller synthesis methods for...
research
∙
05/17/2023
Finding an ε-close Variation of Parameters in Bayesian Networks
This paper addresses the ϵ-close parameter tuning problem for Bayesian N...
research
∙
04/19/2023
On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata
Probabilistic pushdown automata (pPDA) are a natural operational model f...
research
∙
02/13/2023
Lower Bounds for Possibly Divergent Probabilistic Programs
We present a new proof rule for verifying lower bounds on quantities of ...
research
∙
02/01/2023
Exact Probabilistic Inference Using Generating Functions
Probabilistic programs are typically normal-looking programs describing ...
research
∙
11/23/2022
A Calculus for Amortized Expected Runtimes
We develop a weakest-precondition-style calculus à la Dijkstra for reaso...
research
∙
09/20/2022
Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming
A barrier certificate often serves as an inductive invariant that isolat...
research
∙
07/14/2022
Parameter Synthesis in Markov Models: A Gentle Survey
This paper surveys the analysis of parametric Markov models whose transi...
research
∙
07/06/2022
Towards Concurrent Quantitative Separation Logic
In this paper, we develop a novel verification technique to reason about...
research
∙
05/12/2022
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
A desired property of randomized systems, represented by probabilistic p...
research
∙
05/03/2022
Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions
We study discrete probabilistic programs with potentially unbounded loop...
research
∙
03/21/2022
Inductive Synthesis of Finite-State Controllers for POMDPs
We present a novel learning framework to obtain finite-state controllers...
research
∙
02/15/2022
Weighted Programming
We study weighted programming, a programming paradigm for specifying mat...
research
∙
02/06/2022
BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees
Fault trees are a key model in reliability analysis. Classical static fa...
research
∙
01/27/2022
Foundations for Entailment Checking in Quantitative Separation Logic (extended version)
Quantitative separation logic (QSL) is an extension of separation logic ...
research
∙
01/21/2022
Under-Approximating Expected Total Rewards in POMDPs
We consider the problem: is the optimal expected total reward to reach a...
research
∙
12/24/2021
Scenario-Based Verification of Uncertain Parametric MDPs
We consider parametric Markov decision processes (pMDPs) that are augmen...
research
∙
11/08/2021
Gradient-Descent for Randomized Controllers under Partial Observability
Randomization is a powerful technique to create robust controllers, in p...
research
∙
11/05/2021
Model Checking Temporal Properties of Recursive Probabilistic Programs
Probabilistic pushdown automata (pPDA) are a standard operational model ...
research
∙
07/27/2021
The Probabilistic Termination Tool Amber
We describe the Amber tool for proving and refuting the termination of a...
research
∙
07/12/2021
Local Reasoning about Parameterized Reconfigurable Distributed Systems
This paper presents a Hoare-style calculus for formal reasoning about re...
research
∙
06/30/2021
Convex Optimization for Parameter Synthesis in MDPs
Probabilistic model checking aims to prove whether a Markov decision pro...
research
∙
05/29/2021
Fine-Tuning the Odds in Bayesian Networks
This paper proposes various new analysis techniques for Bayes networks i...
research
∙
05/29/2021
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming
A barrier certificate often serves as an inductive invariant that isolat...
research
∙
05/28/2021
Latticed k-Induction with an Application to Probabilistic Programs
We revisit two well-established verification techniques, k-induction and...
research
∙
05/27/2021
Model Repair Revamped: On the Automated Synthesis of Markov Chains
This paper outlines two approaches|based on counterexample-guided abstra...
research
∙
01/29/2021
Inductive Synthesis for Probabilistic Programs Reaches New Horizons
This paper presents a novel method for the automated synthesis of probab...
research
∙
01/28/2021
Probabilistic Data with Continuous Distributions
Statistical models of real world data typically involve continuous proba...
research
∙
11/02/2020
Out of Control: Reducing Probabilistic Models by Control-State Elimination
We present a new, simple technique to reduce state space sizes in probab...
research
∙
10/27/2020
Relatively Complete Verification of Probabilistic Programs
We study a syntax for specifying quantitative "assertions" - functions m...
research
∙
10/26/2020
Multi-objective Optimization of Long-run Average and Total Rewards
This paper presents an efficient procedure for multi-objective model che...
research
∙
10/07/2020
Automated Termination Analysis of Polynomial Probabilistic Programs
The termination behavior of probabilistic programs depends on the outcom...
research
∙
09/28/2020
The Complexity of Reachability in Parametric Markov Decision Processes
This article presents the complexity of reachability decision problems f...
research
∙
07/29/2020
Bayesian Inference by Symbolic Model Checking
This paper applies probabilistic model checking techniques for discrete ...
research
∙
07/13/2020
Generating Functions for Probabilistic Programs
This paper investigates the usage of generating functions (GFs) encoding...
research
∙
06/30/2020
Verification of indefinite-horizon POMDPs
The verification problem in MDPs asks whether, for any policy resolving ...
research
∙
05/18/2020
Weakest Preexpectation Semantics for Bayesian Inference
We present a semantics of a probabilistic while-language with soft condi...
research
∙
05/08/2020
Stochastic Games with Lexicographic Reachability-Safety Objectives
We study turn-based stochastic zero-sum games with lexicographic prefere...
research
∙
04/30/2020
PrIC3: Property Directed Reachability for MDPs
IC3 has been a leap forward in symbolic model checking. This paper propo...
research
∙
04/28/2020
Various Ways to Quantify BDMPs
A Boolean logic driven Markov process (BDMP) is a dependability analysis...
research
∙
03/26/2020
Benchmarking Software Model Checkers on Automotive Code
This paper reports on our experiences with verifying automotive C code b...
research
∙
02/17/2020
The Probabilistic Model Checker Storm
We present the probabilistic model checker Storm. Storm supports the ana...
research
∙
01/17/2020
Generative Datalog with Continuous Distributions
Arguing for the need to combine declarative and probabilistic programmin...
research
∙
12/24/2019
Scenario-Based Verification of Uncertain MDPs
We consider Markov decision processes (MDPs) in which the transition pro...
research
∙
10/24/2019
Simple Strategies in Multi-Objective MDPs (Technical Report)
We consider the verification of multiple expected reward objectives at o...
research
∙
07/19/2019
Are Parametric Markov Chains Monotonic?
This paper presents a simple algorithm to check whether reachability pro...
research
∙
06/17/2019
Multiple Analyses, Requirements Once: simplifying testing & verification in automotive model-based development
In industrial model-based development (MBD) frameworks, requirements are...
research
∙
04/28/2019