{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T06:16:14Z","timestamp":1784182574946,"version":"3.55.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T00:00:00Z","timestamp":1605225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"funder":[{"name":"National Science Foundation","award":["CNS-1065060"],"award-info":[{"award-number":["CNS-1065060"]}]},{"name":"NSF","award":["CNS-1513694"],"award-info":[{"award-number":["CNS-1513694"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,11,13]]},"abstract":"<jats:p>\n            Applying differential privacy at scale requires convenient ways to check that programs computing with sensitive data appropriately preserve privacy. We propose here a fully automated framework for\n            <jats:italic>testing<\/jats:italic>\n            differential privacy, adapting a well-known \u201cpointwise\u201d technique from informal proofs of differential privacy. Our framework, called DPCheck, requires no programmer annotations, handles all previously verified or tested algorithms, and is the first fully automated framework to distinguish correct and buggy implementations of PrivTree, a probabilistically terminating algorithm that has not previously been mechanically checked.\n          <\/jats:p>\n          <jats:p>We analyze the probability of DPCheck mistakenly accepting a non-private program and prove that, theoretically, the probability of false acceptance can be made exponentially small by suitable choice of test size.<\/jats:p>\n          <jats:p>We demonstrate DPCheck\u2019s utility empirically by implementing all benchmark algorithms from prior work on mechanical verification of differential privacy, plus several others and their incorrect variants, and show DPCheck accepts the correct implementations and rejects the incorrect variants.<\/jats:p>\n          <jats:p>We also demonstrate how DPCheck can be deployed in a practical workflow to test differentially privacy for the 2020 US Census Disclosure Avoidance System (DAS).<\/jats:p>","DOI":"10.1145\/3428233","type":"journal-article","created":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:40:14Z","timestamp":1606261214000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Testing differential privacy with dual interpreters"],"prefix":"10.1145","volume":"4","author":[{"given":"Hengchu","family":"Zhang","sequence":"first","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Edo","family":"Roth","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andreas","family":"Haeberlen","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Benjamin C.","family":"Pierce","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aaron","family":"Roth","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158146"},{"key":"e_1_2_2_2_1","unstructured":"Apple. 2017. Apple Diferential Privacy Whitepaper. https:\/\/images.apple.com\/privacy\/docs\/Diferential_Privacy_Overview. pdf  Apple. 2017. Apple Diferential Privacy Whitepaper. https:\/\/images.apple.com\/privacy\/docs\/Diferential_Privacy_Overview. pdf"},{"key":"e_1_2_2_3_1","volume-title":"Eighth ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010 ). 169-178","author":"Axelsson E."},{"key":"e_1_2_2_4_1","volume-title":"Automated Methods for Checking Diferential Privacy. arXiv","author":"Barthe Gilles","year":"1910"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978391"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934554"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243863"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jeconom.2016.01.003"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_10_1","volume-title":"Free Gap Information from the Diferentially Private Sparse Vector and Noisy Max Mechanisms. CoRR abs\/","author":"Ding Zeyu","year":"1904"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243818"},{"key":"e_1_2_2_12_1","volume-title":"Theory of Cryptography","author":"Dwork Cynthia"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1561\/0400000042"},{"key":"e_1_2_2_14_1","unstructured":"Gian Pietro Farina Stephen Chong and Marco Gaboardi. 2017. Relational Symbolic Execution. CoRR abs\/1711.08349 ( 2017 ). arXiv: 1711.08349 http:\/\/arxiv.org\/abs\/1711.08349  Gian Pietro Farina Stephen Chong and Marco Gaboardi. 2017. Relational Symbolic Execution. CoRR abs\/1711.08349 ( 2017 ). arXiv: 1711.08349 http:\/\/arxiv.org\/abs\/1711.08349"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429113"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1536414.1536464"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.29012\/jpc.v4i2.621"},{"key":"e_1_2_2_18_1","unstructured":"Justin Hsu. 2017. Probabilistic Couplings for Probabilistic Reasoning. CoRR abs\/1710.09951 ( 2017 ). arXiv: 1710.09951 http:\/\/arxiv.org\/abs\/1710.09951  Justin Hsu. 2017. Probabilistic Couplings for Probabilistic Reasoning. CoRR abs\/1710.09951 ( 2017 ). arXiv: 1710.09951 http:\/\/arxiv.org\/abs\/1710.09951"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2014.35"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.29012\/jpc.v6i1.634"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.14778\/3055330.3055331"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.1951.10500769"},{"key":"e_1_2_2_24_1","unstructured":"Microsoft. 2017. Collecting telemetry data privately. https:\/\/www.microsoft.com\/en-us\/research\/blog\/collecting-telemetrydata-privately\/  Microsoft. 2017. Collecting telemetry data privately. https:\/\/www.microsoft.com\/en-us\/research\/blog\/collecting-telemetrydata-privately\/"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382264"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1198\/000313008X332421"},{"key":"e_1_2_2_28_1","volume-title":"Abowd","author":"Dajani Aref N.","year":"2017"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360598"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.12688\/gatesopenres.13089.1"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_2_2_32_1","volume-title":"Advances in Neural Information Processing Systems 29","author":"Rogers Ryan M","year":"1921"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.18128\/D010.V10.0"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785668"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40447-4_2"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2015.07.003SI:TFP2011\/12"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364506.2364524"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594340"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314619"},{"key":"e_1_2_2_40_1","volume-title":"William Lam, Damien Desfontaines, Daniel Simmons-Marengo, and Bryant Gipson.","author":"Wilson Royce J","year":"2019"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110254"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009884"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009884"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2882903.2882928"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428233","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428233","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428233","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:57Z","timestamp":1750197777000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428233"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,13]]},"references-count":44,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2020,11,13]]}},"alternative-id":["10.1145\/3428233"],"URL":"https:\/\/doi.org\/10.1145\/3428233","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11,13]]},"assertion":[{"value":"2020-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}