106 citations · 132 across the 10 of their papers we have counts for
11 papers
Elton: Urn Resources for Reasoning about Adversarial Probabilistic Programs
Kwing Hei Li, Alejandro Aguirre, Philipp G. Haselwarter +2
Probabilistic programs are important for many applications. For security applications in particular, one is interested in establishing properties that hold in the presence of arbit…
Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic
Markus de Medeiros, Puming Liu, Kwing Hei Li +3
Most implementations of sampling algorithms for continuous distributions use floating-point numbers, which introduce round-off errors and approximations. These errors can be diffic…
Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)
Philipp G. Haselwarter, Alejandro Aguirre, Simon Oddershede Gregersen +3
Differential privacy is the standard method for privacy-preserving data analysis. The importance of having strong guarantees on the reliability of implementations of differentially…
Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti +1
We present Foxtrot, the first higher-order separation logic for proving contextual refinement of higher-order concurrent probabilistic programs with higher-order local state. From…
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen +3
We present Coneris, the first higher-order concurrent separation logic for reasoning about error probability bounds of higher-order concurrent probabilistic programs with higher-or…
Approximate Relational Reasoning for Higher-Order Probabilistic Programs
Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre +3
Properties such as provable security and correctness for randomized programs are naturally expressed relationally as approximate equivalences. As a result, a number of relational p…
Tachis: Higher-Order Separation Logic with Credits for Expected Costs
Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros +4
We present Tachis, a higher-order separation logic to reason about the expected cost of probabilistic programs. Inspired by the uses of time credits for reasoning about the running…
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros +4
Probabilistic programs often trade accuracy for efficiency, and thus may, with a small probability, return an incorrect result. It is important to obtain precise bounds for the pro…
Formalizing May's Theorem
Kwing Hei Li
This report presents a formalization of May's theorem in the proof assistant Coq. It describes how the theorem statement is first translated into Coq definitions, and how it is sub…
Secure Aggregation for Federated Learning in Flower
Kwing Hei Li, Pedro Porto Buarque de Gusmão, Daniel J. Beutel +1
Federated Learning (FL) allows parties to learn a shared prediction model by delegating the training computation to clients and aggregating all the separately trained models on the…
Flower: A Friendly Federated Learning Research Framework
Daniel J. Beutel, Taner Topal, Akhil Mathur +8
Federated Learning (FL) has emerged as a promising technique for edge devices to collaboratively learn a shared prediction model, while keeping their training data on the device, t…