{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,14]],"date-time":"2026-07-14T22:30:43Z","timestamp":1784068243147,"version":"3.55.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CNS 1553548, CCF 1900924, CCF 1901069, CCF 2007428"],"award-info":[{"award-number":["CNS 1553548, CCF 1900924, CCF 1901069, CCF 2007428"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,1,4]]},"abstract":"<jats:p>\n                    Differential privacy is a mathematical framework for developing statistical computations with provable guarantees of privacy and accuracy. In contrast to the privacy component of differential privacy, which has a clear mathematical and intuitive meaning, the accuracy component of differential privacy does not have a generally accepted definition; accuracy claims of differential privacy algorithms vary from algorithm to algorithm and are not instantiations of a general definition. We identify program discontinuity as a common theme in existing\n                    <jats:italic toggle=\"yes\">ad hoc<\/jats:italic>\n                    definitions and introduce an alternative notion of accuracy parametrized by, what we call, \u2014 the of an input\n                    <jats:italic toggle=\"yes\">x<\/jats:italic>\n                    w.r.t.\u00a0 a deterministic computation\n                    <jats:italic toggle=\"yes\">f<\/jats:italic>\n                    and a distance\n                    <jats:italic toggle=\"yes\">d<\/jats:italic>\n                    , is the minimal distance\n                    <jats:italic toggle=\"yes\">d<\/jats:italic>\n                    (\n                    <jats:italic toggle=\"yes\">x<\/jats:italic>\n                    ,\n                    <jats:italic toggle=\"yes\">y<\/jats:italic>\n                    ) over all\n                    <jats:italic toggle=\"yes\">y<\/jats:italic>\n                    such that\n                    <jats:italic toggle=\"yes\">f<\/jats:italic>\n                    (\n                    <jats:italic toggle=\"yes\">y<\/jats:italic>\n                    )\u2260\n                    <jats:italic toggle=\"yes\">f<\/jats:italic>\n                    (\n                    <jats:italic toggle=\"yes\">x<\/jats:italic>\n                    ). We show that our notion of accuracy subsumes the definition used in theoretical computer science, and captures known accuracy claims for differential privacy algorithms. In fact, our general notion of accuracy helps us prove better claims in some cases. Next, we study the decidability of accuracy. We first show that accuracy is in general undecidable. Then, we define a non-trivial class of probabilistic computations for which accuracy is decidable (unconditionally, or assuming Schanuel\u2019s conjecture). We implement our decision procedure and experimentally evaluate the effectiveness of our approach for generating proofs or counterexamples of accuracy for common algorithms from the literature.\n                  <\/jats:p>","DOI":"10.1145\/3434289","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T12:34:24Z","timestamp":1609763664000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Deciding accuracy of differential privacy schemes"],"prefix":"10.1145","volume":"5","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[{"name":"MPI-SP, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rohit","family":"Chadha","sequence":"additional","affiliation":[{"name":"University of Missouri, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paul","family":"Krogmeier","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"A. Prasad","family":"Sistla","sequence":"additional","affiliation":[{"name":"University of Illinois at Chicago, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99154-2_2"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","unstructured":"Aws Albarghouthi and Justin Hsu. 2018. Synthesizing coupling proofs of diferential privacy. PACMPL 2 POPL ( 2018 ) 58 : 1-58 : 30. https:\/\/doi.org\/10.1145\/3158146 10.1145\/3158146","DOI":"10.1145\/3158146"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394796"},{"key":"e_1_2_1_4_1","volume-title":"Deciding Diferential Privacy for Programs with Finite Inputs and Outputs. CORR abs\/","author":"Barthe Gilles","year":"1910","unstructured":"Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla, and Mahesh Viswanathan. 2020b. Deciding Diferential Privacy for Programs with Finite Inputs and Outputs. CORR abs\/ 1910.04137 ( 2020 ). arXiv: 1910.04137 http:\/\/arxiv.org\/ abs\/ 1910.04137"},{"key":"e_1_2_1_5_1","volume-title":"Deciding Accuracy of Diferential Privacy Schemes. CoRR abs\/","author":"Barthe Gilles","year":"2011","unstructured":"Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, and Mahesh Viswanathan. 2020c. Deciding Accuracy of Diferential Privacy Schemes. CoRR abs\/ 2011.06404 ( 2020 ). arXiv: 2011.06404 https:\/\/arxiv.org\/abs\/ 2011.06404"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_3"},{"key":"e_1_2_1_7_1","volume-title":"International Colloquium on Automata, Languages and Programming (ICALP)","author":"Barthe Gilles","unstructured":"Gilles Barthe, Marco Gaboardi, Benjamin Gr\u00e9goire, Justin Hsu, and Pierre-Yves Strub. 2016b. A program logic for union bounds. In International Colloquium on Automata, Languages and Programming (ICALP), Rome, Italy. arXiv:Yes http:\/\/arxiv.org\/abs\/1602.05681"},{"key":"e_1_2_1_8_1","article-title":"Programming language techniques for diferential privacy","volume":"3","author":"Barthe Gilles","year":"2016","unstructured":"Gilles Barthe, Marco Gaboardi, Justin Hsu, and Benjamin C. Pierce. 2016c. Programming language techniques for diferential privacy. SIGLOG News 3, 1 ( 2016 ), 34-53. https:\/\/dl.acm.org\/citation.cfm?id= 2893591","journal-title":"SIGLOG News"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2492061"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1835804.1835869"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243863"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2450142.2450148"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_2_1_14_1","article-title":"Private and continual release of statistics","volume":"14","author":"Hubert Chan T.-H.","year":"2011","unstructured":"T.-H. Hubert Chan, Elaine Shi, and Dawn Song. 2011. Private and continual release of statistics. ACM Transactions on Information and System Security 14, 3 ( 2011 ), 26. http:\/\/eprint.iacr.org\/ 2010 \/076.pdf","journal-title":"ACM Transactions on Information and System Security"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837639"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_9"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59152-6_27"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243818"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/11681878_14"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1561\/0400000042"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429113"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611973075.90"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_7"},{"key":"e_1_2_1_25_1","unstructured":"Benjamin Lucien Kaminski. 2019. Advanced weakest precondition calculi for probabilistic programs. Ph.D. Dissertation. RWTH Aachen University Germany. http:\/\/publications.rwth-aachen.de\/record\/755408"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934574"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17465-1_8"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ALLERTON.2010.5707120"},{"key":"e_1_2_1_30_1","volume-title":"Introduction to Transcendental Numbers","author":"Lang Serge","unstructured":"Serge Lang. 1966. Introduction to Transcendental Numbers. Addison-Wesley."},{"key":"e_1_2_1_31_1","volume-title":"Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017","author":"Ligett Katrina","year":"2017","unstructured":"Katrina Ligett, Seth Neel, Aaron Roth, Bo Waggoner, and Steven Z. Wu. 2017. Accuracy First: Selecting a Diferential Privacy Level for Accuracy Constrained ERM. In Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, 4-9 December 2017, Long Beach, CA, USA, Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett (Eds.). 2566-2576."},{"key":"e_1_2_1_32_1","first-page":"441","article-title":"On the decidability of the real exponential field. In Kreiseliana. About and Around Georg Kreisel, Piergiorgio Odifreddi (Ed.)","author":"MacIntyre Angus","year":"1996","unstructured":"Angus MacIntyre and Alex J. Wilkie. 1996. On the decidability of the real exponential field. In Kreiseliana. About and Around Georg Kreisel, Piergiorgio Odifreddi (Ed.). A.K. Peters, 441-467.","journal-title":"A.K. Peters"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2011.08.004"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45099-3_17"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_1_37_1","volume-title":"Randomized Algorithms","author":"Motwani Rajeev","unstructured":"Rajeev Motwani and Prabhakar Raghavan. 1995. Randomized Algorithms. Cambridge University Press."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108770750.009"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462179"},{"key":"e_1_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Calvin Smith Justin Hsu and Aws Albarghouthi. 2019. Trace abstraction modulo probability. PACMPL 3 POPL ( 2019 ) 39 : 1-39 : 31. https:\/\/dl.acm.org\/citation.cfm?id= 3290352","DOI":"10.1145\/3290352"},{"key":"e_1_2_1_42_1","volume-title":"A decision method for Elementary Algebra and Geometry","author":"Tarski A.","unstructured":"A. Tarski. 1951. A decision method for Elementary Algebra and Geometry. University of California Press."},{"key":"e_1_2_1_43_1","volume-title":"A Programming Framework for Diferential Privacy with Accuracy Concentration Bounds. CoRR abs\/","author":"Vesga Elisabet Lobo","year":"1909","unstructured":"Elisabet Lobo Vesga, Alejandro Russo, and Marco Gaboardi. 2019. A Programming Framework for Diferential Privacy with Accuracy Concentration Bounds. CoRR abs\/ 1909.07918 ( 2019 ). arXiv: 1909.07918 http:\/\/arxiv.org\/abs\/ 1909.07918"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192408"},{"key":"e_1_2_1_45_1","volume-title":"Reps","author":"Wang Di","year":"2020","unstructured":"Di Wang, Jan Hofmann, and Thomas W. Reps. 2020. Tail Bound Analysis for Probabilistic Programs via Central Moments. CoRR abs\/ 2001.10150 ( 2020 ). arXiv: 2001.10150 https:\/\/arxiv.org\/abs\/ 2001.10150"},{"key":"e_1_2_1_46_1","volume-title":"Statistical Model Checking for Probabilistic Hyperproperties. CoRR abs\/","author":"Wang Yu","year":"1902","unstructured":"Yu Wang, Siddhartha Nalluri, Borzoo Bonakdarpour, and Miroslav Pajic. 2019. Statistical Model Checking for Probabilistic Hyperproperties. CoRR abs\/ 1902.04111 ( 2019 ). arXiv: 1902.04111 http:\/\/arxiv.org\/abs\/ 1902.04111"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009884"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434289","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434289","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434289","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:26:07Z","timestamp":1781853967000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434289"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":47,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434289"],"URL":"https:\/\/doi.org\/10.1145\/3434289","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}