{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:20:28Z","timestamp":1776316828657,"version":"3.50.1"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2013,11,1]],"date-time":"2013-11-01T00:00:00Z","timestamp":1383264000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Spanish project","award":["TIN2009-14599 DESAFIOS 10"],"award-info":[{"award-number":["TIN2009-14599 DESAFIOS 10"]}]},{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","award":["FP7-256980 NESSoS, FP7-229599 AMAROUT"],"award-info":[{"award-number":["FP7-256980 NESSoS, FP7-229599 AMAROUT"]}],"id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]},{"name":"French project","award":["ANR SESUR-012 SCALP"],"award-info":[{"award-number":["ANR SESUR-012 SCALP"]}]},{"name":"Madrid Regional project","award":["S2009TIC-1465 PROMETIDOS"],"award-info":[{"award-number":["S2009TIC-1465 PROMETIDOS"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2013,11]]},"abstract":"<jats:p>Differential privacy is a notion of confidentiality that allows useful computations on sensible data while protecting the privacy of individuals. Proving differential privacy is a difficult and error-prone task that calls for principled approaches and tool support. Approaches based on linear types and static analysis have recently emerged; however, an increasing number of programs achieve privacy using techniques that fall out of their scope. Examples include programs that aim for weaker, approximate differential privacy guarantees and programs that achieve differential privacy without using any standard mechanisms. Providing support for reasoning about the privacy of such programs has been an open problem.<\/jats:p>\n          <jats:p>We report on CertiPriv, a machine-checked framework for reasoning about differential privacy built on top of the Coq proof assistant. The central component of CertiPriv is a quantitative extension of probabilistic relational Hoare logic that enables one to derive differential privacy guarantees for programs from first principles. We demonstrate the applicability of CertiPriv on a number of examples whose formal analysis is out of the reach of previous techniques. In particular, we provide the first machine-checked proofs of correctness of the Laplacian, Gaussian, and exponential mechanisms and of the privacy of randomized and streaming algorithms from the literature.<\/jats:p>","DOI":"10.1145\/2492061","type":"journal-article","created":{"date-parts":[[2013,11,12]],"date-time":"2013-11-12T15:29:09Z","timestamp":1384270149000},"page":"1-49","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":62,"title":["Probabilistic Relational Reasoning for Differential Privacy"],"prefix":"10.1145","volume":"35","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[{"name":"IMDEA Software Institute"}]},{"given":"Boris","family":"K\u00f6pf","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute"}]},{"given":"Federico","family":"Olmedo","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute"}]},{"given":"Santiago","family":"Zanella-B\u00e9guelin","sequence":"additional","affiliation":[{"name":"Microsoft Research"}]}],"member":"320","published-online":{"date-parts":[[2013,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382249"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27864-1_10"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111046"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.09.002"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2009.18"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_14"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2011.20"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_8"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1009380.1009669"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/2033036.2033043"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/2021296.2021319"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103670"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2013.26"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85174-5_25"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1595696.1595700"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.02.040"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1880999.1881044"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025131"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1370628.1370629"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1891823.1891830"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70630-4_6"},{"key":"e_1_2_1_24_1","volume-title":"information, and machine-assisted proof. Tech. rep. UCAMCL-TR-785","author":"Coble Aaron R.","unstructured":"Aaron R. Coble. 2010. Anonymity, information, and machine-assisted proof. Tech. rep. UCAMCL-TR-785. University of Cambridge, Computer Laboratory. http:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-785.pdf."},{"key":"e_1_2_1_25_1","unstructured":"The Coq Development Team. 2010. The coq proof assistant reference manual version 8.3. http:\/\/coq.inria.fr."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/646066.676656"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2008.42"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/1297689.1297691"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1791834.1791836"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1866739.1866758"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/11761679_29"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/11681878_14"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2010.12"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90065-5"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1287\/moor.22.4.793"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/1873601.1873691"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/2028067.2028100"},{"key":"e_1_2_1_38_1","volume-title":"Formal verification of probabilistic algorithms. Tech. rep. UCAM-CL-TR-566","author":"Hurd Joe","unstructured":"Joe Hurd. 2003. Formal verification of probabilistic algorithms. Tech. rep. UCAM-CL-TR-566, University of Cambridge, Computer Laboratory. http:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-566.pdf."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.08.005"},{"key":"e_1_2_1_41_1","volume-title":"Larsen","author":"Jonsson Bengt","year":"2001","unstructured":"Bengt Jonsson, Wang Yi, and Kim G. Larsen. 2001. Probabilistic extensions of process algebras. In Handbook of Process Algebra. Elsevier, Amsterdam, 685--710."},{"key":"e_1_2_1_42_1","unstructured":"Shiva Prasad Kasiviswanathan and Adam Smith. 2008. A note on differential privacy: Defining resistance to arbitrary side information. Cryptology ePrint archive report 2008\/144."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1989323.1989345"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_1_45_1","volume-title":"Combinatorial Optimization: Networks and Matroids. Holt, Rinehart and Winston","author":"Lawler Eugene L.","year":"1976","unstructured":"Eugene L. Lawler. 1976. Combinatorial Optimization: Networks and Matroids. Holt, Rinehart and Winston, New York."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1559845.1559850"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2007.41"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_27"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/2033939.2033959"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03356-8_8"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.5555\/130819"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2488608.2488652"},{"key":"e_1_2_1_54_1","volume-title":"A simple probabilistic approximation algorithm for vertex cover. Tech. rep. TR-404","author":"Pitt Leonard","unstructured":"Leonard Pitt. 1985. A simple probabilistic approximation algorithm for vertex cover. Tech. rep. TR-404, Yale University."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503288"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/800141.804647"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855711.1855731"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.5555\/794200.795151"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2007.8"},{"key":"e_1_2_1_61_1","series-title":"Lecture Notes in Computer Science","volume-title":"Integer Programming and Combinatorial Optimization","author":"Tardos Eva","unstructured":"Eva Tardos and Kevin Wayne. 1998. Simple generalized maximum flow algorithms. In Integer Programming and Combinatorial Optimization. Lecture Notes in Computer Science, vol. 1412, Springer, 310--324."},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_24"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.015"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_5"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2492061","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2492061","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:39:02Z","timestamp":1750235942000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2492061"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11]]},"references-count":63,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,11]]}},"alternative-id":["10.1145\/2492061"],"URL":"https:\/\/doi.org\/10.1145\/2492061","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,11]]},"assertion":[{"value":"2012-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-11-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}