research
∙
09/14/2023
A Deductive Verification Infrastructure for Probabilistic Programs
This paper presents a quantitative program verification infrastructure f...
share
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
∙
01/27/2022
Foundations for Entailment Checking in Quantitative Separation Logic (extended version)
Quantitative separation logic (QSL) is an extension of separation logic ...
research
∙
10/26/2021
Flexible Refinement Proofs in Separation Logic
Refinement transforms an abstract system model into a concrete, executab...
research
∙
05/28/2021
Latticed k-Induction with an Application to Probabilistic Programs
We revisit two well-established verification techniques, k-induction and...
research
∙
10/27/2020
Relatively Complete Verification of Probabilistic Programs
We study a syntax for specifying quantitative "assertions" - functions m...
research
∙
04/30/2020
PrIC3: Property Directed Reachability for MDPs
IC3 has been a leap forward in symbolic model checking. This paper propo...
research
∙
02/04/2020
Complete Entailment Checking for Separation Logic with Inductive Definitions
In [A], we proposed a novel decision procedure for entailment checking i...
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