Document Open Access Logo

A Theory AB Toolbox

Authors Marco Gaboardi, Justin Hsu

PDF
Thumbnail PDF

File

LIPIcs.SNAPL.2015.129.pdf
  • Filesize: 430 kB
  • 11 pages

Document Identifiers

Author Details

Marco Gaboardi
Justin Hsu

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.SNAPL.2015.129

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.

Subject Classification

Keywords
  • Verification
  • randomized algorithms

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. First SIGPLAN Workshop on Probabilistic and Approximate Computing (APPROX'14). Co-located with PLDI 2014, Edinburgh, Scotland., 2014. Google Scholar
  2. Philippe Audebaud and Christine Paulin-Mohring. Proofs of randomized algorithms in coq. Science of Computer Programming, 74(8):568-589, 2009. Google Scholar
  3. Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, and Santiago Zanella-Béguelin. Probabilistic relational verification for cryptographic implementations. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), San Diego, California, pages 193-206, 2014. Google Scholar
  4. Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, and Pierre-Yves Strub. Higher-order approximate relational refinement types for mechanism design and differential privacy. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Mumbai, India, 2015. Google Scholar
  5. Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella Béguelin. Computer-aided security proofs for the working cryptographer. In Proceedings of the 31st annual conference on Advances in Cryptology (CRYPTO), pages 71-90, 2011. Google Scholar
  6. Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Béguelin. Probabilistic relational reasoning for differential privacy. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Philadelphia, Pennsylvania, pages 97-110, 2012. Google Scholar
  7. Michael Carbin, Deokhwan Kim, Sasa Misailovic, and Martin C Rinard. Proving acceptability properties of relaxed nondeterministic approximate programs. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Beijing, China, pages 169-180, 2012. Google Scholar
  8. T.-H. Hubert Chan, Elaine Shi, and Dawn Song. Private and continual release of statistics. ACM Transactions on Information and System Security, 14(3):26, 2011. Google Scholar
  9. Devdatt P Dubhashi and Alessandro Panconesi. Concentration of measure for the analysis of randomized algorithms. Cambridge University Press, 2009. Google Scholar
  10. Cynthia Dwork, Moni Naor, Toniann Pitassi, and Guy N. Rothblum. Differential privacy under continual observation. In ACM SIGACT Symposium on Theory of Computing (STOC), Cambridge, Massachusetts, pages 715-724, 2010. Google Scholar
  11. Paul Erdős. Graph theory and probability. Canadian Journal of Mathematics, 11:34-38, 1959. Google Scholar
  12. Paul Erdos and László Lovász. Problems and results on 3-chromatic hypergraphs and some related questions. Infinite and finite sets, 10:609-627, 1975. Google Scholar
  13. Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C Pierce. Linear dependent types for differential privacy. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Rome, Italy, pages 357-370, 2013. Google Scholar
  14. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, et al. A machine-checked proof of the odd order theorem. In Interactive Theorem Proving, pages 163-179. Springer, 2013. Google Scholar
  15. Michael Kearns, Mallesh Pai, Aaron Roth, and Jonathan Ullman. Mechanism design in large games: Incentives and privacy. In ACM SIGACT Innovations in Theoretical Computer Science (ITCS), Princeton, New Jersey, pages 403-410, 2014. Google Scholar
  16. Jason Reed and Benjamin C Pierce. Distance makes the types grow stronger: A calculus for differential privacy. In ACM SIGPLAN International Conference on Functional Programming (ICFP), Baltimore, Maryland, 2010. Google Scholar
  17. Ryan M Rogers and Aaron Roth. Asymptotically truthful equilibrium selection in large congestion games. In ACM SIGecom Conference on Economics and Computation (EC), Palo Alto, California, pages 771-782, 2014. Google Scholar
  18. Adrian Sampson, Pavel Panchekha, Todd Mytkowicz, Kathryn S McKinley, Dan Grossman, and Luis Ceze. Expressing and verifying probabilistic assertions. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Edinburgh, Scotland, pages 112-122, 2014. Google Scholar
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 About DROPS Imprint Privacy Contact