79 citations · 242 across the 12 of their papers we have counts for
12 papers · 1 filter
Synthesizing Backward Error Bounds, Backward
Laura Zielinski, Justin Hsu
Backward stability is a desirable property for a well-designed numerical algorithm: given an input, a backward stable floating-point program produces the exact output for a nearby…
Cutting the Cake: A Language for Fair Division
Noah Bertram, Alex Levinson, Justin Hsu
The fair division literature in economics considers how to divide resources between multiple agents such that the allocation is envy-free: each agent receives their favorite piece.…
Separated and Shared Effects in Higher-Order Languages
Pedro H. Azevedo de Amorim, Justin Hsu
Effectful programs interact in ways that go beyond simple input-output, making compositional reasoning challenging. Existing work has shown that when such programs are ``separate''…
Symbolic Execution for Randomized Programs
Zachary Susag, Sumit Lahiri, Justin Hsu +1
We propose a symbolic execution method for programs that can draw random samples. In contrast to existing work, our method can verify randomized programs with unknown inputs and ca…
A Probabilistic Separation Logic
Gilles Barthe, Justin Hsu, Kevin Liao
Probabilistic independence is a useful concept for describing the result of random sampling---a basic operation in all probabilistic languages---and for reasoning about groups of r…
Scalable Verification of Probabilistic Networks
Steffen Smolka, Praveen Kumar, David M Kahn +4
This paper presents McNetKAT, a scalable tool for verifying probabilistic network programs. McNetKAT is based on a new semantics for the guarded and history-free fragment of Probab…