279 citations · 1.1k across the 46 of their papers we have counts for
15 papers · 1 filter
A Formal Model for Secure Multiparty Computation
Amy Rathore, Marina Blanton, Marco Gaboardi +1
Although Secure Multiparty Computation (SMC) has seen considerable development in recent years, its use is challenging, resulting in complex code which obscures whether the securit…
Bunched Fuzz: Sensitivity for Vector Metrics
june wunder, Arthur Azevedo de Amorim, Patrick Baillot +1
Program sensitivity measures the distance between the outputs of a program when run on two related inputs. This notion, which plays a key role in areas such as data privacy and opt…
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…
On Incorrectness Logic and Kleene Algebra with Top and Tests
Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi
Kleene algebra with tests (KAT) is a foundational equational framework for reasoning about programs, which has found applications in program transformations, networking and compile…
Coupled Relational Symbolic Execution for Differential Privacy
Gian Pietro Farina, Stephen Chong, Marco Gaboardi
Differential privacy is a de facto standard in data privacy with applications in the private and public sectors. Most of the techniques that achieve differential privacy are based…
Bidirectional Type Checking for Relational Properties
Ezgi Çiçek, Weihao Qu, Gilles Barthe +2
Relational type systems have been designed for several applications including information flow, differential privacy, and cost analysis. In order to achieve the best results, these…
Relational Cost Analysis for Functional-Imperative Programs
Weihao Qu, Marco Gaboardi, Deepak Garg
Relational cost analysis aims at formally establishing bounds on the difference in the evaluation costs of two programs. As a particular case, one can also use relational cost anal…
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…
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus
Alejandro Aguirre, Gilles Barthe, Lars Birkedal +3
We extend the simply-typed guarded -calculus with discrete probabilities and endow it with a program logic for reasoning about relational properties of guarded probabilistic com…
Relational Symbolic Execution
Gian Pietro Farina, Stephen Chong, Marco Gaboardi
Symbolic execution is a classical program analysis technique used to show that programs satisfy or violate given specifications. In this work we generalize symbolic execution to su…
Approximate Span Liftings
Tetsuya Sato, Gilles Barthe, Marco Gaboardi +2
We develop new abstractions for reasoning about relaxations of differential privacy: Rényi differential privacy, zero-concentrated differential privacy, and truncated concentrated…
A Relational Logic for Higher-Order Programs
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi +2
Relational program verification is a variant of program verification where one can reason about two programs and as a special case about two executions of a single program on diffe…
A Semantic Account of Metric Preservation
Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu +2
Program sensitivity measures how robust a program is to small changes in its input, and is a fundamental notion in domains ranging from differential privacy to cyber-physical syste…
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias +3
Mechanism design is the study of algorithm design in which the inputs to the algorithm are controlled by strategic agents, who must be incentivized to faithfully report them. Unlik…
Linear Dependent Types for Domain Specific Program Analysis (Extended Abstract)
Marco Gaboardi
In this tutorial I will present how a combination of linear and dependent type can be useful to describe different properties about higher order programs. Linear types have been pr…