{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:39:34Z","timestamp":1780994374433,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":34,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,7,8]],"date-time":"2020-07-08T00:00:00Z","timestamp":1594166400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,7,8]]},"DOI":"10.1145\/3373718.3394796","type":"proceedings-article","created":{"date-parts":[[2020,5,26]],"date-time":"2020-05-26T00:23:18Z","timestamp":1590452598000},"page":"141-154","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Deciding Differential Privacy for Programs with Finite Inputs and Outputs"],"prefix":"10.1145","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[{"name":"MPI Security and Privacy and IMDEA, Software Institute, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rohit","family":"Chadha","sequence":"additional","affiliation":[{"name":"University of Missouri, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vishal","family":"Jagannath","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Campaign, 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-Campaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,7,8]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"POPL","author":"Albarghouthi Aws","year":"2018","unstructured":"Aws Albarghouthi and Justin Hsu . 2018. Synthesizing coupling proofs of differential privacy. PACMPL 2 , POPL ( 2018 ), 58:1--58:30. Aws Albarghouthi and Justin Hsu. 2018. Synthesizing coupling proofs of differential privacy. PACMPL 2, POPL (2018), 58:1--58:30."},{"key":"e_1_3_2_1_2_1","volume-title":"Principles of Model Checking","author":"Baier C.","unstructured":"C. Baier and J.-P. Katoen . 2008. Principles of Model Checking . MIT Press . C. Baier and J.-P. Katoen. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_3_2_1_3_1","unstructured":"Gilles Barthe Rohit Chadha Vishal Jagannath A. Prasad Sistla and Mahesh Viswanathan. 2019. Differential Privacy Checker (DiPC). https:\/\/anonymous.4open.science\/repository\/febcbe47-1c53-41db- be91-ea98b4cf18c1\/.  Gilles Barthe Rohit Chadha Vishal Jagannath A. Prasad Sistla and Mahesh Viswanathan. 2019. Differential Privacy Checker (DiPC). https:\/\/anonymous.4open.science\/repository\/febcbe47-1c53-41db- be91-ea98b4cf18c1\/."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Gilles Barthe Rohit Chadha Vishal Jagannath A. Prasad Sistla and Mahesh Viswanathan. 2020. Deciding Differential Privacy for Programs with Finite Inputs and Outputs. arXiv:1910.04137 [cs.CR]  Gilles Barthe Rohit Chadha Vishal Jagannath A. Prasad Sistla and Mahesh Viswanathan. 2020. Deciding Differential Privacy for Programs with Finite Inputs and Outputs. arXiv:1910.04137 [cs.CR]","DOI":"10.1145\/3373718.3394796"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978391"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934554"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2893582.2893591"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2492061"},{"key":"e_1_3_2_1_9_1","volume-title":"Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, David Lie, Mohammad Mannan, Michael Backes, and XiaoFeng Wang (Eds.). ACM, 508--524","author":"Bichsel Benjamin","unstructured":"Benjamin Bichsel , Timon Gehr , Dana Drachsler-Cohen , Petar Tsankov , and Martin T. Vechev . 2018. DP-Finder: Finding Differential Privacy Violations by Sampling and Optimization . In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, David Lie, Mohammad Mannan, Michael Backes, and XiaoFeng Wang (Eds.). ACM, 508--524 . Benjamin Bichsel, Timon Gehr, Dana Drachsler-Cohen, Petar Tsankov, and Martin T. Vechev. 2018. DP-Finder: Finding Differential Privacy Violations by Sampling and Optimization. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, David Lie, Mohammad Mannan, Michael Backes, and XiaoFeng Wang (Eds.). ACM, 508--524."},{"key":"e_1_3_2_1_10_1","first-page":"26","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 . 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.","journal-title":"ACM Transactions on Information and System Security"},{"key":"e_1_3_2_1_11_1","volume-title":"Generalized Bisimulation Metrics. In 35th International Conference on Concurrency Theory, CONCUR","author":"Chatzikokolakis Konstantinos","year":"2014","unstructured":"Konstantinos Chatzikokolakis , Daniel Gebler , Catuscia Palamidessi , and Lili Xu . 2014 . Generalized Bisimulation Metrics. In 35th International Conference on Concurrency Theory, CONCUR 2014. Springer Berlin Heidelberg, 32--46. Konstantinos Chatzikokolakis, Daniel Gebler, Catuscia Palamidessi, and Lili Xu. 2014. Generalized Bisimulation Metrics. In 35th International Conference on Concurrency Theory, CONCUR 2014. Springer Berlin Heidelberg, 32--46."},{"key":"e_1_3_2_1_12_1","volume-title":"Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018 (Lecture Notes in Computer Science), Shuvendu K","author":"Chistikov Dmitry","unstructured":"Dmitry Chistikov , Andrzej S. Murawski , and David Purser . 2018. Bisimilarity Distances for Approximate Differential Privacy . In Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018 (Lecture Notes in Computer Science), Shuvendu K . Lahiri and Chao Wang (Eds.), Vol. 11138 . Springer , 194--210. Dmitry Chistikov, Andrzej S. Murawski, and David Purser. 2018. Bisimilarity Distances for Approximate Differential Privacy. In Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018 (Lecture Notes in Computer Science), Shuvendu K. Lahiri and Chao Wang (Eds.), Vol. 11138. Springer, 194--210."},{"key":"e_1_3_2_1_13_1","volume-title":"Asymmetric Distances for Approximate Differential Privacy. In 30th International Conference on Concurrency Theory, CONCUR 2019 (LIPIcs), Wan Fokkink and Rob van Glabbeek (Eds.)","volume":"140","author":"Chistikov Dmitry","year":"2019","unstructured":"Dmitry Chistikov , Andrzej S. Murawski , and David Purser . 2019 . Asymmetric Distances for Approximate Differential Privacy. In 30th International Conference on Concurrency Theory, CONCUR 2019 (LIPIcs), Wan Fokkink and Rob van Glabbeek (Eds.) , Vol. 140 . Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 10:1--10:17. Dmitry Chistikov, Andrzej S. Murawski, and David Purser. 2019. Asymmetric Distances for Approximate Differential Privacy. In 30th International Conference on Concurrency Theory, CONCUR 2019 (LIPIcs), Wan Fokkink and Rob van Glabbeek (Eds.), Vol. 140. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 10:1--10:17."},{"key":"e_1_3_2_1_14_1","volume-title":"Probability and Stochastics","author":"Cinlar Erhan","unstructured":"Erhan Cinlar . 2011. Probability and Stochastics . Springer . Erhan Cinlar. 2011. Probability and Stochastics. Springer."},{"key":"e_1_3_2_1_15_1","volume-title":"Marco Gaboardi, and Justin Hsu.","author":"de Amorim Arthur Azevedo","year":"2015","unstructured":"Arthur Azevedo de Amorim , Emilio Jes\u00fas Gallego Arias , Marco Gaboardi, and Justin Hsu. 2015 . Really Natural Linear Indexed Type Checking. http:\/\/arxiv.org\/abs\/1503.04522. CoRR abs\/1503.04522 (2015). arXiv:1503.04522 Arthur Azevedo de Amorim, Emilio Jes\u00fas Gallego Arias, Marco Gaboardi, and Justin Hsu. 2015. Really Natural Linear Indexed Type Checking. http:\/\/arxiv.org\/abs\/1503.04522. CoRR abs\/1503.04522 (2015). arXiv:1503.04522"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785715"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243818"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11681878_14"},{"key":"e_1_3_2_1_19_1","volume-title":"ACM SIGACT Symposium on Theory of Computing (STOC)","author":"Dwork Cynthia","unstructured":"Cynthia Dwork , Moni Naor , Omer Reingold , Guy N. Rothblum , and Salil P. Vadhan . 2009. On the complexity of differentially private data release: efficient algorithms and hardness results . In ACM SIGACT Symposium on Theory of Computing (STOC) , Bethesda, Maryland. 381--390. Cynthia Dwork, Moni Naor, Omer Reingold, Guy N. Rothblum, and Salil P. Vadhan. 2009. On the complexity of differentially private data release: efficient algorithms and hardness results. In ACM SIGACT Symposium on Theory of Computing (STOC), Bethesda, Maryland. 381--390."},{"key":"e_1_3_2_1_20_1","first-page":"3","article-title":"The Algorithmic Foundations of Differential Privacy","volume":"9","author":"Dwork Cynthia","year":"2014","unstructured":"Cynthia Dwork and Aaron Roth . 2014 . The Algorithmic Foundations of Differential Privacy . Foundations and Trends in Theoretical Computer Science 9 , 3 - 4 (2014), 211--407. Cynthia Dwork and Aaron Roth. 2014. The Algorithmic Foundations of Differential Privacy. Foundations and Trends in Theoretical Computer Science 9, 3-4 (2014), 211--407.","journal-title":"Foundations and Trends in Theoretical Computer Science"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429113"},{"key":"e_1_3_2_1_22_1","volume-title":"47th International Colloquium on Automata, Languages and Programming (ICALP' 20)","author":"Gaboardi Marco","year":"2019","unstructured":"Marco Gaboardi , Kobbi Nissim , and David Purser . 2019 . The Complexity of Verifying Circuits as Differentially Private. http:\/\/arxiv.org\/abs\/1911.03272. CoRR abs\/1911.03272 (2019). arXiv:1911.03272 To Appear in 47th International Colloquium on Automata, Languages and Programming (ICALP' 20) , 2020. Marco Gaboardi, Kobbi Nissim, and David Purser. 2019. The Complexity of Verifying Circuits as Differentially Private. http:\/\/arxiv.org\/abs\/1911.03272. CoRR abs\/1911.03272 (2019). arXiv:1911.03272 To Appear in 47th International Colloquium on Automata, Languages and Programming (ICALP' 20), 2020."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611973075.90"},{"key":"e_1_3_2_1_24_1","volume-title":"TCC 2012, Taormina, Sicily, Italy, March 19-21, 2012. Proceedings (Lecture Notes in Computer Science), Ronald Cramer (Ed.)","volume":"7194","author":"Gupta Anupam","year":"2012","unstructured":"Anupam Gupta , Aaron Roth , and Jonathan Ullman . 2012 . Iterative Constructions and Private Data Release. In Theory of Cryptography - 9th Theory of Cryptography Conference , TCC 2012, Taormina, Sicily, Italy, March 19-21, 2012. Proceedings (Lecture Notes in Computer Science), Ronald Cramer (Ed.) , Vol. 7194 . Springer, 339--356. Anupam Gupta, Aaron Roth, and Jonathan Ullman. 2012. Iterative Constructions and Private Data Release. In Theory of Cryptography - 9th Theory of Cryptography Conference, TCC 2012, Taormina, Sicily, Italy, March 19-21, 2012. Proceedings (Lecture Notes in Computer Science), Ronald Cramer (Ed.), Vol. 7194. Springer, 339--356."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2010.85"},{"key":"e_1_3_2_1_26_1","volume-title":"APLAS 2018 (Lecture Notes in Computer Science), Sukyoung Ryu (Ed.)","volume":"11275","author":"Liu Depeng","year":"2018","unstructured":"Depeng Liu , Bow-Yaw Wang , and Lijun Zhang . 2018 . Model Checking Differentially Private Properties. In Programming Languages and Systems - 16th Asian Symposium , APLAS 2018 (Lecture Notes in Computer Science), Sukyoung Ryu (Ed.) , Vol. 11275 . Springer, 394--414. Depeng Liu, Bow-Yaw Wang, and Lijun Zhang. 2018. Model Checking Differentially Private Properties. In Programming Languages and Systems - 16th Asian Symposium, APLAS 2018 (Lecture Notes in Computer Science), Sukyoung Ryu (Ed.), Vol. 11275. Springer, 394--414."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.14778\/3055330.3055331"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2011.08.004"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2007.66"},{"key":"e_1_3_2_1_30_1","volume-title":"The Category of Markov Kernels. Electronic Notes in Theoretical Computer Science 22 (12","author":"Panangaden Prakash","year":"1999","unstructured":"Prakash Panangaden . 1999. The Category of Markov Kernels. Electronic Notes in Theoretical Computer Science 22 (12 1999 ), 171--187. Prakash Panangaden. 1999. The Category of Markov Kernels. Electronic Notes in Theoretical Computer Science 22 (12 1999), 171--187."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","unstructured":"J. M. Rutten M. Kwiatkowska G. Norman and D. Parker. 2004. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. AMS.  J. M. Rutten M. Kwiatkowska G. Norman and D. Parker. 2004. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. AMS.","DOI":"10.1090\/crmm\/023"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314619"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009884"}],"event":{"name":"LICS '20: 35th Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"Saarbr\u00fccken Germany","acronym":"LICS '20","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"]},"container-title":["Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394796","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3373718.3394796","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:36Z","timestamp":1750197756000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394796"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,8]]},"references-count":34,"alternative-id":["10.1145\/3373718.3394796","10.1145\/3373718"],"URL":"https:\/\/doi.org\/10.1145\/3373718.3394796","relation":{},"subject":[],"published":{"date-parts":[[2020,7,8]]},"assertion":[{"value":"2020-07-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}