
Local Reasoning about Parameterized Reconfigurable Distributed Systems
This paper presents a Hoarestyle calculus for formal reasoning about re...
read it

Convex Optimization for Parameter Synthesis in MDPs
Probabilistic model checking aims to prove whether a Markov decision pro...
read it

FineTuning the Odds in Bayesian Networks
This paper proposes various new analysis techniques for Bayes networks i...
read it

Synthesizing Invariant Barrier Certificates via DifferenceofConvex Programming
A barrier certificate often serves as an inductive invariant that isolat...
read it

Latticed kInduction with an Application to Probabilistic Programs
We revisit two wellestablished verification techniques, kinduction and...
read it

Model Repair Revamped: On the Automated Synthesis of Markov Chains
This paper outlines two approachesbased on counterexampleguided abstra...
read it

Inductive Synthesis for Probabilistic Programs Reaches New Horizons
This paper presents a novel method for the automated synthesis of probab...
read it

Probabilistic Data with Continuous Distributions
Statistical models of real world data typically involve continuous proba...
read it

Out of Control: Reducing Probabilistic Models by ControlState Elimination
We present a new, simple technique to reduce state space sizes in probab...
read it

Relatively Complete Verification of Probabilistic Programs
We study a syntax for specifying quantitative "assertions"  functions m...
read it

Multiobjective Optimization of Longrun Average and Total Rewards
This paper presents an efficient procedure for multiobjective model che...
read it

Automated Termination Analysis of Polynomial Probabilistic Programs
The termination behavior of probabilistic programs depends on the outcom...
read it

The Complexity of Reachability in Parametric Markov Decision Processes
This article presents the complexity of reachability decision problems f...
read it

Bayesian Inference by Symbolic Model Checking
This paper applies probabilistic model checking techniques for discrete ...
read it

Generating Functions for Probabilistic Programs
This paper investigates the usage of generating functions (GFs) encoding...
read it

Verification of indefinitehorizon POMDPs
The verification problem in MDPs asks whether, for any policy resolving ...
read it

Weakest Preexpectation Semantics for Bayesian Inference
We present a semantics of a probabilistic whilelanguage with soft condi...
read it

Stochastic Games with Lexicographic ReachabilitySafety Objectives
We study turnbased stochastic zerosum games with lexicographic prefere...
read it

PrIC3: Property Directed Reachability for MDPs
IC3 has been a leap forward in symbolic model checking. This paper propo...
read it

Various Ways to Quantify BDMPs
A Boolean logic driven Markov process (BDMP) is a dependability analysis...
read it

Benchmarking Software Model Checkers on Automotive Code
This paper reports on our experiences with verifying automotive C code b...
read it

The Probabilistic Model Checker Storm
We present the probabilistic model checker Storm. Storm supports the ana...
read it

Generative Datalog with Continuous Distributions
Arguing for the need to combine declarative and probabilistic programmin...
read it

ScenarioBased Verification of Uncertain MDPs
We consider Markov decision processes (MDPs) in which the transition pro...
read it

Simple Strategies in MultiObjective MDPs (Technical Report)
We consider the verification of multiple expected reward objectives at o...
read it

Are Parametric Markov Chains Monotonic?
This paper presents a simple algorithm to check whether reachability pro...
read it

Multiple Analyses, Requirements Once: simplifying testing & verification in automotive modelbased development
In industrial modelbased development (MBD) frameworks, requirements are...
read it

CounterexampleDriven Synthesis for Probabilistic Program Sketches
Probabilistic programs are key to deal with uncertainty in e.g. controll...
read it

On the Complexity of Reachability in Parametric Markov Decision Processes
This paper studies parametric Markov decision processes (pMDPs), an exte...
read it

Aiming Low Is Harder  Inductive Proof Rules for Lower Bounds on Weakest Preexpectations in Probabilistic Program Verification
We present a new inductive proof rule for reasoning about lower bounds o...
read it

Parameter Synthesis for Markov Models
Markov chain analysis is a key technique in reliability engineering. A p...
read it

Safety Analysis for Vehicle Guidance Systems with Dynamic Fault Trees
This paper considers the designphase safety analysis of vehicle guidanc...
read it

Shepherding Hordes of Markov Chains
This paper considers large families of Markov chains (MCs) that are defi...
read it

Kantorovich Continuity of Probabilistic Programs
The Kantorovich metric is a canonical lifting of a distance from sets to...
read it

The Partially Observable Games We Play for Cyber Deception
Progressively intricate cyber infiltration mechanisms have made conventi...
read it

ParameterIndependent Strategies for pMDPs via POMDPs
Markov Decision Processes (MDPs) are a popular class of models suitable ...
read it

Sound Value Iteration
Computing reachability probabilities is at the heart of probabilistic mo...
read it

One Net Fits All: A unifying semantics of Dynamic Fault Trees using GSPNs
Dynamic Fault Trees (DFTs) are a prominent model in reliability engineer...
read it

Quantitative Separation Logic
We present quantitative separation logic (QSL). In contrast to classical...
read it

How long, O Bayesian network, will I sample thee? A program analysis perspective on expected sampling times
Bayesian networks (BNs) are probabilistic graphical models for describin...
read it

A New Proof Rule for AlmostSure Termination
An important question for a probabilistic program is whether the probabi...
read it

Permissive FiniteState Controllers of POMDPs using Parameter Synthesis
We study finitestate controllers (FSCs) for partially observable Markov...
read it

Motion Planning under Partial Observability using GameBased Abstraction
We study motion planning problems where agents move inside environments ...
read it

Probabilistic Model Checking for Complex Cognitive Tasks  A case study in humanrobot interaction
This paper proposes to use probabilistic model checking to synthesize op...
read it

The Probabilistic Model Checker Storm (Extended Abstract)
We present a new probabilistic model checker Storm. Using stateofthea...
read it
JoostPieter Katoen
is this you? claim profile