Simple relational correctness proofs for static analyses and program transformations

By Nick Benton. 2004

376 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Signal Processing

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Signal Processing

Citations in the corpus

Proving Differential Privacy via Probabilistic Couplings (2016, neutral): “Conceived as a probabilistic variant of Benton’s relational Hoare logic [9], apRHL has been used to verify differential privacy for examples using the standard composition theorems.”
Proving Differential Privacy in Hoare Logic (2014, background): “On a more practical side, it would be interesting to implement our transformation for a realistic setting, for instance modeling thePINQ language [30].”
Satisfiability modulo counting: a new approach for analyzing privacy properties (2014, background): “Others have studied relational variants of the Hoare logic [10] with applications to information ﬂow analysis.”
Computer-Aided Verification for Mechanism Design (2015, background): “Recently, Brânzei and Procaccia [6] define verifiably truthful mechanisms.”
Relational Reasoning via Probabilistic Coupling (2015, methodology): “More broadly, our work occupies a middle ground between the two main approaches to relational verification: (i) encoding the two programs as a single program and reasoning about the single program (techniques include include cross-products [12], self-composition [1], and product programs [3]); and (”
Formal certification of code-based cryptographic proofs (2009, methodology): “The correctness of optim is proved using a mixture of the techniques of [10] and [11, 26]: we express the validity of th e information contained in the analysis domain using a predic ate Valid(δ, m) that states the agreement between the compile time abstract values inδ and the runtime memory m.”
Coupling proofs are probabilistic product programs (2016, background): “Program equivalence is one of the original motivation for relational program logics [17].”
Probabilistic relational reasoning for differential privacy (2012, methodology): “A seminal paper [7] develops a relational Hoare logic (RHL) for a core imperative programming language and shows how it can be used to reason about information flow properties of programs.”