Search Results

Documents authored by Gaboardi, Marco

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.157
Domain Reasoning in TopKAT

Authors: Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
TopKAT is the algebraic theory of Kleene algebra with tests (KAT) extended with a top element. Compared to KAT, one pleasant feature of TopKAT is that, in relational models, the top element allows us to express the domain and codomain of a relation. This enables several applications in program logics, such as proving under-approximate specifications or reachability properties of imperative programs. However, while TopKAT inherits many pleasant features of KATs, such as having a decidable equational theory, it is incomplete with respect to relational models. In other words, there are properties that hold true of all relational TopKATs but cannot be proved with the axioms of TopKAT. This issue is potentially worrisome for program-logic applications, in which relational models play a key role. In this paper, we further investigate the completeness properties of TopKAT with respect to relational models. We show that TopKAT is complete with respect to (co)domain comparison of KAT terms, but incomplete when comparing the (co)domain of arbitrary TopKAT terms. Since the encoding of under-approximate specifications in TopKAT hinges on this type of formula, the aforementioned incompleteness results have a limited impact when using TopKAT to reason about such specifications.
Cite as

Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi. Domain Reasoning in TopKAT. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 157:1-157:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{zhang_et_al:LIPIcs.ICALP.2024.157,
  author =	{Zhang, Cheng and de Amorim, Arthur Azevedo and Gaboardi, Marco},
  title =	{{Domain Reasoning in TopKAT}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{157:1--157:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.157},
  URN =		{urn:nbn:de:0030-drops-203003},
  doi =		{10.4230/LIPIcs.ICALP.2024.157},
  annote =	{Keywords: Kleene algebra, Kleene Algebra With Tests, Kleene Algebra With Domain, Kleene Algebra With Top and Tests, Completeness, Decidability}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.FSCD.2023
LIPIcs, Volume 260, FSCD 2023, Complete Volume

Authors: Marco Gaboardi and Femke van Raamsdonk

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
LIPIcs, Volume 260, FSCD 2023, Complete Volume
Cite as

8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 1-658, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Proceedings{gaboardi_et_al:LIPIcs.FSCD.2023,
  title =	{{LIPIcs, Volume 260, FSCD 2023, Complete Volume}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{1--658},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023},
  URN =		{urn:nbn:de:0030-drops-179830},
  doi =		{10.4230/LIPIcs.FSCD.2023},
  annote =	{Keywords: LIPIcs, Volume 260, FSCD 2023, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.FSCD.2023.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Marco Gaboardi and Femke van Raamsdonk

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{gaboardi_et_al:LIPIcs.FSCD.2023.0,
  author =	{Gaboardi, Marco and van Raamsdonk, Femke},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{0:i--0:xviii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.0},
  URN =		{urn:nbn:de:0030-drops-179849},
  doi =		{10.4230/LIPIcs.FSCD.2023.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.ITP.2022.30
Formalizing Algorithmic Bounds in the Query Model in EasyCrypt

Authors: Alley Stoughton, Carol Chen, Marco Gaboardi, and Weihao Qu

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
We use the EasyCrypt proof assistant to formalize the adversarial approach to proving lower bounds for computational problems in the query model. This is done using a lower bound game between an algorithm and adversary, in which the adversary answers the algorithm’s queries in a way that makes the algorithm issue at least the desired number of queries. A complementary upper bound game is used for proving upper bounds of algorithms; here the adversary incrementally and adaptively realizes an algorithm’s input. We prove a natural connection between the lower and upper bound games, and apply our framework to three computational problems, including searching in an ordered list and comparison-based sorting, giving evidence for the generality of our notion of algorithm and the usefulness of our framework.
Cite as

Alley Stoughton, Carol Chen, Marco Gaboardi, and Weihao Qu. Formalizing Algorithmic Bounds in the Query Model in EasyCrypt. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 30:1-30:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{stoughton_et_al:LIPIcs.ITP.2022.30,
  author =	{Stoughton, Alley and Chen, Carol and Gaboardi, Marco and Qu, Weihao},
  title =	{{Formalizing Algorithmic Bounds in the Query Model in EasyCrypt}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{30:1--30:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.30},
  URN =		{urn:nbn:de:0030-drops-167399},
  doi =		{10.4230/LIPIcs.ITP.2022.30},
  annote =	{Keywords: query model, lower bound, upper bound, adversary argument, EasyCrypt}
}
Document
DOI: 10.4230/LIPIcs.FORC.2022.1
Controlling Privacy Loss in Sampling Schemes: An Analysis of Stratified and Cluster Sampling

Authors: Mark Bun, Jörg Drechsler, Marco Gaboardi, Audra McMillan, and Jayshree Sarathy

Published in: LIPIcs, Volume 218, 3rd Symposium on Foundations of Responsible Computing (FORC 2022)

Abstract
Sampling schemes are fundamental tools in statistics, survey design, and algorithm design. A fundamental result in differential privacy is that a differentially private mechanism run on a simple random sample of a population provides stronger privacy guarantees than the same algorithm run on the entire population. However, in practice, sampling designs are often more complex than the simple, data-independent sampling schemes that are addressed in prior work. In this work, we extend the study of privacy amplification results to more complex, data-dependent sampling schemes. We find that not only do these sampling schemes often fail to amplify privacy, they can actually result in privacy degradation. We analyze the privacy implications of the pervasive cluster sampling and stratified sampling paradigms, as well as provide some insight into the study of more general sampling designs.
Cite as

Mark Bun, Jörg Drechsler, Marco Gaboardi, Audra McMillan, and Jayshree Sarathy. Controlling Privacy Loss in Sampling Schemes: An Analysis of Stratified and Cluster Sampling. In 3rd Symposium on Foundations of Responsible Computing (FORC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 218, pp. 1:1-1:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bun_et_al:LIPIcs.FORC.2022.1,
  author =	{Bun, Mark and Drechsler, J\"{o}rg and Gaboardi, Marco and McMillan, Audra and Sarathy, Jayshree},
  title =	{{Controlling Privacy Loss in Sampling Schemes: An Analysis of Stratified and Cluster Sampling}},
  booktitle =	{3rd Symposium on Foundations of Responsible Computing (FORC 2022)},
  pages =	{1:1--1:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-226-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{218},
  editor =	{Celis, L. Elisa},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FORC.2022.1},
  URN =		{urn:nbn:de:0030-drops-165243},
  doi =		{10.4230/LIPIcs.FORC.2022.1},
  annote =	{Keywords: privacy, differential privacy, survey design, survey sampling}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.129
The Complexity of Verifying Loop-Free Programs as Differentially Private

Authors: Marco Gaboardi, Kobbi Nissim, and David Purser

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Abstract
We study the problem of verifying differential privacy for loop-free programs with probabilistic choice. Programs in this class can be seen as randomized Boolean circuits, which we will use as a formal model to answer two different questions: first, deciding whether a program satisfies a prescribed level of privacy; second, approximating the privacy parameters a program realizes. We show that the problem of deciding whether a program satisfies ε-differential privacy is coNP^#P-complete. In fact, this is the case when either the input domain or the output range of the program is large. Further, we show that deciding whether a program is (ε,δ)-differentially private is coNP^#P-hard, and in coNP^#P for small output domains, but always in coNP^{#P^#P}. Finally, we show that the problem of approximating the level of differential privacy is both NP-hard and coNP-hard. These results complement previous results by Murtagh and Vadhan [Jack Murtagh and Salil P. Vadhan, 2016] showing that deciding the optimal composition of differentially private components is #P-complete, and that approximating the optimal composition of differentially private components is in P.
Cite as

Marco Gaboardi, Kobbi Nissim, and David Purser. The Complexity of Verifying Loop-Free Programs as Differentially Private. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 129:1-129:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{gaboardi_et_al:LIPIcs.ICALP.2020.129,
  author =	{Gaboardi, Marco and Nissim, Kobbi and Purser, David},
  title =	{{The Complexity of Verifying Loop-Free Programs as Differentially Private}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{129:1--129:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.129},
  URN =		{urn:nbn:de:0030-drops-125362},
  doi =		{10.4230/LIPIcs.ICALP.2020.129},
  annote =	{Keywords: differential privacy, program verification, probabilistic programs}
}
Document
DOI: 10.4230/DagRep.7.7.72
Resource Bound Analysis (Dagstuhl Seminar 17291)

Authors: Marco Gaboardi, Jan Hoffman, Reinhard Wilhelm, and Florian Zuleger

Published in: Dagstuhl Reports, Volume 7, Issue 7 (2018)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 17291 "Resource Bound Analysis". Resource-bound analysis is studied in formal methods and programming languages at different levels of abstraction. The goal of the Dagstuhl seminar was to bring together leading researchers with different backgrounds in resource-bound analysis to address challenging open problems and to facilitate communication across research areas.
Cite as

Marco Gaboardi, Jan Hoffman, Reinhard Wilhelm, and Florian Zuleger. Resource Bound Analysis (Dagstuhl Seminar 17291). In Dagstuhl Reports, Volume 7, Issue 7, pp. 72-87, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{gaboardi_et_al:DagRep.7.7.72,
  author =	{Gaboardi, Marco and Hoffman, Jan and Wilhelm, Reinhard and Zuleger, Florian},
  title =	{{Resource Bound Analysis (Dagstuhl Seminar 17291)}},
  pages =	{72--87},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{7},
  number =	{7},
  editor =	{Gaboardi, Marco and Hoffman, Jan and Wilhelm, Reinhard and Zuleger, Florian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.7.7.72},
  URN =		{urn:nbn:de:0030-drops-84241},
  doi =		{10.4230/DagRep.7.7.72},
  annote =	{Keywords: quantitative analysis, resource-bound analysis, WCET}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2017.1
Type Systems for the Relational Verification of Higher Order Programs (Invited Talk)

Authors: Marco Gaboardi

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract
Relational program verification is a variant of program verification where one focuses on guaranteeing properties about the executions of two programs, and as a special case about two executions of a single program on different inputs. Relational verification becomes particularly interesting when non-functional aspects of a computation, like probabilities or resource cost, are considered. Several approached to relational program verification have been developed, from relational program logics to relational abstract interpretation. In this talk, I will introduce two approaches to relational program verification for higher-order computations based on the use of type systems. The first approach consists in developing powerful type system where a rich language of assertions can be used to express complex relations between two programs. The second approach consists in developing more restrictive type systems enriched with effects expressing in a lightweight way relations between different runs of the same program. I will discuss the pros and cons of these two approaches on a concrete example: relational cost analysis, which aims at giving a bound on the difference in cost of running two programs, and as a special case the difference in cost of two executions of a single program on different inputs.
Cite as

Marco Gaboardi. Type Systems for the Relational Verification of Higher Order Programs (Invited Talk). In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{gaboardi:LIPIcs.FSCD.2017.1,
  author =	{Gaboardi, Marco},
  title =	{{Type Systems for the Relational Verification of Higher Order Programs}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.1},
  URN =		{urn:nbn:de:0030-drops-77429},
  doi =		{10.4230/LIPIcs.FSCD.2017.1},
  annote =	{Keywords: Relational verification, refinement types, type and effect systems, complexity analysis}
}
Document
DOI: 10.4230/DagRep.6.3.59
Language Based Verification Tools for Functional Programs (Dagstuhl Seminar 16131)

Authors: Marco Gaboardi, Suresh Jagannathan, Ranjit Jhala, and Stephanie Weirich

Published in: Dagstuhl Reports, Volume 6, Issue 3 (2016)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 16131 "Language Based Verification Tools for Functional Programs". This seminar is motivated by two converging trends in computing -- the increasing reliance on software has led to an increased interest in seeking formal, reliable means of ensuring that programs possess crucial correctness properties, and the dramatic increase in adoption of higher-order functional languages due to the web, multicore and "big data" revolutions. While the research community has studied the problem of language based verification for imperative and first-order programs for decades – yielding important ideas like Floyd-Hoare Logics, Abstract Interpretation, Model Checking, and Separation Logic and so on – it is only relatively recently, that proposals have emerged for language baseverification tools for functional and higher-order programs. These techniques include advanced type systems, contract systems, model checking and program analyses specially tailored to exploit the structure of functional languages. These proposals are from groups based in diverse research communities, attacking the problem from different angles, yielding techniques with complementary strengths. This seminar brought diverse set of researchers together so that we could: compare the strengths and limitations of different approaches, discuss ways to unify the complementary advantages of different techniques, both conceptually and in tools, share challenging open problems and application areas where verification may be most effective, identify novel ways of using verification techniques for other software engineering tasks such as code search or synthesis, and improve the pedagogy and hence adoption of such techniques.
Cite as

Marco Gaboardi, Suresh Jagannathan, Ranjit Jhala, and Stephanie Weirich. Language Based Verification Tools for Functional Programs (Dagstuhl Seminar 16131). In Dagstuhl Reports, Volume 6, Issue 3, pp. 59-77, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{gaboardi_et_al:DagRep.6.3.59,
  author =	{Gaboardi, Marco and Jagannathan, Suresh and Jhala, Ranjit and Weirich, Stephanie},
  title =	{{Language Based Verification Tools for Functional Programs (Dagstuhl Seminar 16131)}},
  pages =	{59--77},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{6},
  number =	{3},
  editor =	{Gaboardi, Marco and Jagannathan, Suresh and Jhala, Ranjit and Weirich, Stephanie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.6.3.59},
  URN =		{urn:nbn:de:0030-drops-61494},
  doi =		{10.4230/DagRep.6.3.59},
  annote =	{Keywords: Functional Programming, Type Systems, Contracts, Dependent Types, Model Checking, Program Analysis}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.107
A Program Logic for Union Bounds

Authors: Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
We propose a probabilistic Hoare logic aHL based on the union bound, a tool from basic probability theory. While the union bound is simple, it is an extremely common tool for analyzing randomized algorithms. In formal verification terms, the union bound allows flexible and compositional reasoning over possible ways an algorithm may go wrong. It also enables a clean separation between reasoning about probabilities and reasoning about events, which are expressed as standard first-order formulas in our logic. Notably, assertions in our logic are non-probabilistic, even though we can conclude probabilistic facts from the judgments. Our logic can also prove accuracy properties for interactive programs, where the program must produce intermediate outputs as soon as pieces of the input arrive, rather than accessing the entire input at once. This setting also enables adaptivity, where later inputs may depend on earlier intermediate outputs. We show how to prove accuracy for several examples from the differential privacy literature, both interactive and non-interactive.
Cite as

Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. A Program Logic for Union Bounds. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 107:1-107:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{barthe_et_al:LIPIcs.ICALP.2016.107,
  author =	{Barthe, Gilles and Gaboardi, Marco and Gr\'{e}goire, Benjamin and Hsu, Justin and Strub, Pierre-Yves},
  title =	{{A Program Logic for Union Bounds}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{107:1--107:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.107},
  URN =		{urn:nbn:de:0030-drops-62425},
  doi =		{10.4230/LIPIcs.ICALP.2016.107},
  annote =	{Keywords: Probabilistic Algorithms, Accuracy, Formal Verification, Hoare Logic, Union Bound}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.120
Sensitivity of Counting Queries

Authors: Myrto Arapinis, Diego Figueira, and Marco Gaboardi

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
In the context of statistical databases, the release of accurate statistical information about the collected data often puts at risk the privacy of the individual contributors. The goal of differential privacy is to maximise the utility of a query while protecting the individual records in the database. A natural way to achieve differential privacy is to add statistical noise to the result of the query. In this context, a mechanism for releasing statistical information is thus a trade-off between utility and privacy. In order to balance these two "conflicting" requirements, privacy preserving mechanisms calibrate the added noise to the so-called sensitivity of the query, and thus a precise estimate of the sensitivity of the query is necessary to determine the amplitude of the noise to be added. In this paper, we initiate a systematic study of sensitivity of counting queries over relational databases. We first observe that the sensitivity of a Relational Algebra query with counting is not computable in general, and that while the sensitivity of Conjunctive Queries with counting is computable, it becomes unbounded as soon as the query includes a join. We then consider restricted classes of databases (databases with constraints), and study the problem of computing the sensitivity of a query given such constraints. We are able to establish bounds on the sensitivity of counting conjunctive queries over constrained databases. The kind of constraints studied here are: functional dependencies and cardinality dependencies. The latter is a natural generalisation of functional dependencies that allows us to provide tight bounds on the sensitivity of counting conjunctive queries.
Cite as

Myrto Arapinis, Diego Figueira, and Marco Gaboardi. Sensitivity of Counting Queries. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 120:1-120:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{arapinis_et_al:LIPIcs.ICALP.2016.120,
  author =	{Arapinis, Myrto and Figueira, Diego and Gaboardi, Marco},
  title =	{{Sensitivity of Counting Queries}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{120:1--120:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.120},
  URN =		{urn:nbn:de:0030-drops-62552},
  doi =		{10.4230/LIPIcs.ICALP.2016.120},
  annote =	{Keywords: Differential privacy, sensitivity, relational algebra}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2015.129
A Theory AB Toolbox

Authors: Marco Gaboardi and Justin Hsu

Published in: LIPIcs, Volume 32, 1st Summit on Advances in Programming Languages (SNAPL 2015)

Abstract
Randomized algorithms are a staple of the theoretical computer science literature. By careful use of randomness, algorithms can achieve properties that are simply not possible with deterministic algorithms. Today, these properties are proved on paper, by theoretical computer scientists; we investigate formally verifying these proofs. The main challenges are two: proofs about algorithms can be quite complex, using various facts from probability theory; and proofs are highly customized - two proofs of the same property for two algorithms can be completely different. To overcome these challenges, we propose taking inspiration from paper proofs, by building common tools - abstractions, reasoning principles, perhaps even notations - into a formal verification toolbox. To give an idea of our approach, we consider three common patterns in paper proofs: the union bound, concentration bounds, and martingale arguments.
Cite as

Marco Gaboardi and Justin Hsu. A Theory AB Toolbox. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 129-139, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{gaboardi_et_al:LIPIcs.SNAPL.2015.129,
  author =	{Gaboardi, Marco and Hsu, Justin},
  title =	{{A Theory AB Toolbox}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{129--139},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-80-4},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{32},
  editor =	{Ball, Thomas and Bodík, Rastislav and Krishnamurthi, Shriram and Lerner, Benjamin S. and Morriset, Greg},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2015.129},
  URN =		{urn:nbn:de:0030-drops-50225},
  doi =		{10.4230/LIPIcs.SNAPL.2015.129},
  annote =	{Keywords: Verification, randomized algorithms}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact