279 citations · 1.4k across the 46 of their papers we have counts for
53 papers
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…
P4BID: Information Flow Control in P4
Karuna Grewal, Loris D'Antoni, Justin Hsu
Modern programmable network switches can implement custom applications using efficient packet processing hardware, and the programming language P4 provides high-level constructs to…
A Separation Logic for Negative Dependence
Jialu Bao, Marco Gaboardi, Justin Hsu +1
Formal reasoning about hashing-based probabilistic data structures often requires reasoning about random variables where when one variable gets larger (such as the number of elemen…
Data-Driven Invariant Learning for Probabilistic Programs
Jialu Bao, Nitesh Trivedi, Drashti Pathak +2
Morgan and McIver's weakest pre-expectation framework is one of the most well-established methods for deductive verification of probabilistic programs. Roughly, the idea is to gene…
A Quantum Interpretation of Bunched Logic for Quantum Separation Logic
Li Zhou, Gilles Barthe, Justin Hsu +2
We propose a model of the substructural logic of Bunched Implications (BI) that is suitable for reasoning about quantum states. In our model, the separating conjunction of BI descr…
Learning Differentially Private Mechanisms
Subhajit Roy, Justin Hsu, Aws Albarghouthi
Differential privacy is a formal, mathematical definition of data privacy that has gained traction in academia, industry, and government. The task of correctly constructing differe…
Robust Mean Estimation on Highly Incomplete Data with Arbitrary Outliers
Lunjia Hu, Omer Reingold
We study the problem of robustly estimating the mean of a -dimensional distribution given examples, where most coordinates of every example may be missing and $\varepsilon N…
Analyzing Accuracy Loss in Randomized Smoothing Defenses
Yue Gao, Harrison Rosenberg, Kassem Fawaz +2
Recent advances in machine learning (ML) algorithms, especially deep neural networks (DNNs), have demonstrated remarkable success (sometimes exceeding human-level performance) on s…
Advances and Open Problems in Federated Learning
Peter Kairouz, H. Brendan McMahan, Brendan Avent +56
Federated learning (FL) is a machine learning setting where many clients (e.g. mobile devices or whole organizations) collaboratively train a model under the orchestration of a cen…
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…
Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time
Steffen Smolka, Nate Foster, Justin Hsu +3
Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union () and iteration () operations from KAT to pre…
Hypothesis Testing Interpretations and Renyi Differential Privacy
Borja Balle, Gilles Barthe, Marco Gaboardi +2
Differential privacy is a de facto standard in data privacy, with applications in the public and private sectors. A way to explain differential privacy, which is particularly appea…
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…
Data Poisoning against Differentially-Private Learners: Attacks and Defenses
Yuzhe Ma, Xiaojin Zhu, Justin Hsu
Data poisoning attacks aim to manipulate the model produced by a learning algorithm by adversarially modifying the training set. We consider differential privacy as a defensive mea…
Fake News Detection via NLP is Vulnerable to Adversarial Attacks
Zhixuan Zhou, Huankang Guan, Meghana Moorthy Bhat +1
News plays a significant role in shaping people's beliefs and opinions. Fake news has always been a problem, which wasn't exposed to the mass public until the past election cycle f…
A Pre-Expectation Calculus for Probabilistic Sensitivity
Alejandro Aguirre, Gilles Barthe, Justin Hsu +3
Sensitivity properties describe how changes to the input of a program affect the output, typically by upper bounding the distance between the outputs of two runs by a monotone func…
Relational Proofs for Quantum Programs
Gilles Barthe, Justin Hsu, Mingsheng Ying +2
Relational verification of quantum programs has many potential applications in quantum and post-quantum security and other domains. We propose a relational program logic for quantu…
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…