279 citations · 1.4k across the 46 of their papers we have counts for
7 papers · 1 filter
Trace Abstraction Modulo Probability
Calvin Smith, Justin Hsu, Aws Albarghouthi
We propose trace abstraction modulo probability, a proof technique for verifying high-probability accuracy guarantees of probabilistic programs. Our proofs overapproximate the set…
Formal verification of higher-order probabilistic programs
Tetsuya Sato, Alejandro Aguirre, Gilles Barthe +3
Probabilistic programming provides a convenient lingua franca for writing succinct and rigorous descriptions of probabilistic models and inference tasks. Several probabilistic prog…
Probabilistic Relational Reasoning via Metrics
Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu +1
The Fuzz programming language [Reed and Pierce, 2010] uses an elegant linear type system combined with a monad-like type to express and reason about probabilistic sensitivity prope…
Convex Language Semantics for Nondeterministic Probabilistic Automata
Gerco van Heerdt, Justin Hsu, Joël Ouaknine +1
We explore language semantics for automata combining probabilistic and nondeterministic behavior. We first show that there are precisely two natural semantics for probabilistic aut…
Constraint-Based Synthesis of Coupling Proofs
Aws Albarghouthi, Justin Hsu
Proof by coupling is a classical technique for proving properties about pairs of randomized algorithms by carefully relating (or coupling) two probabilistic executions. In this pap…
An Assertion-Based Program Logic for Probabilistic Programs
Gilles Barthe, Thomas Espitau, Marco Gaboardi +3
Research on deductive verification of probabilistic programs has considered expectation-based logics, where pre- and post-conditions are real-valued functions on states, and assert…
Almost Sure Productivity
Alejandro Aguirre, Gilles Barthe, Justin Hsu +1
We define Almost Sure Productivity (ASP), a probabilistic generalization of the productivity condition for coinductively defined structures. Intuitively, a probabilistic coinductiv…