research
∙
09/14/2023
A Deductive Verification Infrastructure for Probabilistic Programs
This paper presents a quantitative program verification infrastructure f...
share
research
∙
08/15/2023
The 19th International Workshop on Termination (WST 2023): Preface, Invited Talk Abstract, and Tool Descriptions
This report contains the proceedings of the 19th International Workshop ...
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
∙
11/23/2022
A Calculus for Amortized Expected Runtimes
We develop a weakest-precondition-style calculus à la Dijkstra for reaso...
research
∙
05/12/2022
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
A desired property of randomized systems, represented by probabilistic p...
research
∙
02/15/2022
Weighted Programming
We study weighted programming, a programming paradigm for specifying mat...
research
∙
02/14/2022
Quantitative Strongest Post
We present a novel strongest-postcondition-style calculus for quantitati...
research
∙
05/28/2021
Latticed k-Induction with an Application to Probabilistic Programs
We revisit two well-established verification techniques, k-induction and...
research
∙
01/28/2021
Probabilistic Data with Continuous Distributions
Statistical models of real world data typically involve continuous proba...
research
∙
10/27/2020
Relatively Complete Verification of Probabilistic Programs
We study a syntax for specifying quantitative "assertions" - functions m...
research
∙
07/13/2020
Generating Functions for Probabilistic Programs
This paper investigates the usage of generating functions (GFs) encoding...
research
∙
04/30/2020
PrIC3: Property Directed Reachability for MDPs
IC3 has been a leap forward in symbolic model checking. This paper propo...
research
∙
01/17/2020
Generative Datalog with Continuous Distributions
Arguing for the need to combine declarative and probabilistic programmin...
research
∙
04/01/2019
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...
research
∙
01/19/2019
Kantorovich Continuity of Probabilistic Programs
The Kantorovich metric is a canonical lifting of a distance from sets to...
research
∙
02/28/2018
Quantitative Separation Logic
We present quantitative separation logic (QSL). In contrast to classical...
research
∙
02/28/2018
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...
research
∙
11/09/2017