{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,17]],"date-time":"2026-02-17T12:07:23Z","timestamp":1771330043993,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T00:00:00Z","timestamp":1559952000000},"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":[[2019,6,8]]},"DOI":"10.1145\/3314221.3314619","type":"proceedings-article","created":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:02:18Z","timestamp":1559941338000},"page":"655-669","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":33,"title":["Proving differential privacy with shadow execution"],"prefix":"10.1145","author":[{"given":"Yuxin","family":"Wang","sequence":"first","affiliation":[{"name":"Pennsylvania State University, USA"}]},{"given":"Zeyu","family":"Ding","sequence":"additional","affiliation":[{"name":"Pennsylvania State University, USA"}]},{"given":"Guanhong","family":"Wang","sequence":"additional","affiliation":[{"name":"Pennsylvania State University, USA"}]},{"given":"Daniel","family":"Kifer","sequence":"additional","affiliation":[{"name":"Pennsylvania State University, USA"}]},{"given":"Danfeng","family":"Zhang","sequence":"additional","affiliation":[{"name":"Pennsylvania State University, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,6,8]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3219819.3226070"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158146"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2013.26"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1009380.1009669"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978391"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2014.36"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677000"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934554"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103670"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_8"},{"key":"e_1_3_2_2_11_1","first-page":"184","volume-title":"Proceedings of the 23rd International Conference on Computer Aided Verification (CAV'11)","author":"Beyer Dirk","unstructured":"Dirk Beyer and M. Erkan Keremoglu . 2011. CPACHECKER: A Tool for Configurable Software Verification . In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV'11) . Springer-Verlag, Berlin, Heidelberg , 184 - 190 . Dirk Beyer and M. Erkan Keremoglu. 2011. CPACHECKER: A Tool for Configurable Software Verification. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV'11). Springer-Verlag, Berlin, Heidelberg, 184-190."},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243863"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53641-4_24"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31759-0_19"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243818"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11761679_29"},{"key":"e_1_3_2_2_19_1","volume-title":"Theory of Cryptography","author":"Dwork Cynthia","unstructured":"Cynthia Dwork , Frank McSherry , Kobbi Nissim , and Adam Smith . 2006. Calibrating Noise to Sensitivity in Private Data Analysis . In Theory of Cryptography , Shai Halevi and Tal Rabin (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 265-284. Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam Smith. 2006. Calibrating Noise to Sensitivity in Private Data Analysis. In Theory of Cryptography, Shai Halevi and Tal Rabin (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 265-284."},{"key":"e_1_3_2_2_20_1","first-page":"3","article-title":"The algorithmic foundations of differential privacy","volume":"9","author":"Dwork Cynthia","year":"2014","unstructured":"Cynthia Dwork , Aaron Roth , 2014 . The algorithmic foundations of differential privacy . Theoretical Computer Science 9 , 3 - 4 (2014), 211-407. Cynthia Dwork, Aaron Roth, et al. 2014. The algorithmic foundations of differential privacy. Theoretical Computer Science 9, 3-4 (2014), 211-407.","journal-title":"Theoretical Computer Science"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677005"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660348"},{"key":"e_1_3_2_2_23_1","volume-title":"Article arXiv:1711.08349 (Nov","author":"Farina Gian Pietro","year":"2017","unstructured":"Gian Pietro Farina , Stephen Chong , and Marco Gaboardi . 2017. Relational Symbolic Execution. arXiv e-prints , Article arXiv:1711.08349 (Nov 2017 ). Gian Pietro Farina, Stephen Chong, and Marco Gaboardi. 2017. Relational Symbolic Execution. arXiv e-prints, Article arXiv:1711.08349 (Nov 2017)."},{"key":"e_1_3_2_2_24_1","first-page":"249","volume-title":"Property Testing For Differential Privacy. 2018 56th Annual Allerton Conference on Communication, Control, and Computing (Allerton)","author":"Anna","year":"2018","unstructured":"Anna C. Gilbert and Audra McMillan. 2018 . Property Testing For Differential Privacy. 2018 56th Annual Allerton Conference on Communication, Control, and Computing (Allerton) ( 2018 ), 249 - 258 . Anna C. Gilbert and Audra McMillan. 2018. Property Testing For Differential Privacy. 2018 56th Annual Allerton Conference on Communication, Control, and Computing (Allerton) (2018), 249-258."},{"key":"e_1_3_2_2_25_1","first-page":"2339","volume-title":"Proceedings of the 25th International Conference on Neural Information Processing Systems -","volume":"2","author":"Hardt Moritz","year":"2012","unstructured":"Moritz Hardt , Katrina Ligett , and Frank McSherry . 2012 . A Simple and Practical Algorithm for Differentially Private Data Release . In Proceedings of the 25th International Conference on Neural Information Processing Systems - Volume 2 (NIPS'12). Curran Associates Inc., USA , 2339 - 2347 . Moritz Hardt, Katrina Ligett, and Frank McSherry. 2012. A Simple and Practical Algorithm for Differentially Private Data Release. In Proceedings of the 25th International Conference on Neural Information Processing Systems - Volume 2 (NIPS'12). Curran Associates Inc., USA, 2339-2347."},{"key":"e_1_3_2_2_26_1","first-page":"79","volume-title":"On Flow-sensitive Security Types. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '06)","author":"Hunt Sebastian","year":"2006","unstructured":"Sebastian Hunt and David Sands . 2006 . On Flow-sensitive Security Types. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '06) . ACM, New York, NY, USA , 79 - 90 . Sebastian Hunt and David Sands. 2006. On Flow-sensitive Security Types. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '06). ACM, New York, NY, USA, 79-90."},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3187009.3177733"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.14778\/3055330.3055331"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2007.41"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1559845.1559850"},{"key":"e_1_3_2_2_32_1","volume-title":"R\u00e9nyi Differential Privacy. In 2017 IEEE 30th Computer Security Foundations Symposium (CSF). 263-275","author":"Mironov I.","year":"2017","unstructured":"I. Mironov . 2017 . R\u00e9nyi Differential Privacy. In 2017 IEEE 30th Computer Security Foundations Symposium (CSF). 263-275 . I. Mironov. 2017. R\u00e9nyi Differential Privacy. In 2017 IEEE 30th Computer Security Foundations Symposium (CSF). 263-275."},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2213836.2213876"},{"key":"e_1_3_2_2_34_1","volume-title":"Privacy Law Scholars Conf.","author":"Nissim Kobbi","year":"2017","unstructured":"Kobbi Nissim , Thomas Steinke , Alexandra Wood , Micah Altman , Aaron Bembenek , Mark Bun , Marco Gaboardi , David R O'Brien , and Salil Vadhan . 2017 . Differential privacy: A primer for a non-technical audience . In Privacy Law Scholars Conf. Kobbi Nissim, Thomas Steinke, Alexandra Wood, Micah Altman, Aaron Bembenek, Mark Bun, Marco Gaboardi, David R O'Brien, and Salil Vadhan. 2017. Differential privacy: A primer for a non-technical audience. In Privacy Law Scholars Conf."},{"key":"e_1_3_2_2_35_1","first-page":"20","volume-title":"Proceedings of the 7th USENIX Conference on Networked Systems Design and Implementation (NSDI'10)","author":"Roy Indrajit","year":"2010","unstructured":"Indrajit Roy , Srinath T. V. Setty , Ann Kilzer , Vitaly Shmatikov , and Emmett Witchel . 2010 . Airavat: Security and Privacy for MapReduce . In Proceedings of the 7th USENIX Conference on Networked Systems Design and Implementation (NSDI'10) . USENIX Association, Berkeley, CA, USA , 20 - 20 . Indrajit Roy, Srinath T. V. Setty, Ann Kilzer, Vitaly Shmatikov, and Emmett Witchel. 2010. Airavat: Security and Privacy for MapReduce. In Proceedings of the 7th USENIX Conference on Networked Systems Design and Implementation (NSDI'10). USENIX Association, Berkeley, CA, USA, 20-20."},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_3_2_2_37_1","article-title":"Learning with Privacy at Scale","volume":"1","author":"Privacy Team Apple Differential","year":"2017","unstructured":"Apple Differential Privacy Team . 2017 . Learning with Privacy at Scale . Apple Machine Learning Journal 1 , 8 (2017). Apple Differential Privacy Team. 2017. Learning with Privacy at Scale. Apple Machine Learning Journal 1, 8 (2017).","journal-title":"Apple Machine Learning Journal"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_24"},{"key":"e_1_3_2_2_39_1","volume-title":"Formal Verification of Differential Privacy for Interactive Systems (Extended Abstract). Electronic Notes in Theoretical Computer Science 276 (Sept","author":"Tschantz Michael Carl","year":"2011","unstructured":"Michael Carl Tschantz , Dilsun Kaynar , and Anupam Datta . 2011. Formal Verification of Differential Privacy for Interactive Systems (Extended Abstract). Electronic Notes in Theoretical Computer Science 276 (Sept . 2011 ), 61-79. Michael Carl Tschantz, Dilsun Kaynar, and Anupam Datta. 2011. Formal Verification of Differential Privacy for Interactive Systems (Extended Abstract). Electronic Notes in Theoretical Computer Science 276 (Sept. 2011), 61-79."},{"key":"e_1_3_2_2_40_1","volume-title":"Article arXiv:1903.12254 (Mar","author":"Wang Yuxin","year":"2019","unstructured":"Yuxin Wang , Zeyu Ding , Guanhong Wang , Daniel Kifer , and Danfeng Zhang . 2019. Proving Differential Privacy with Shadow Execution. arXiv e-prints , Article arXiv:1903.12254 (Mar 2019 ). Yuxin Wang, Zeyu Ding, Guanhong Wang, Daniel Kifer, and Danfeng Zhang. 2019. Proving Differential Privacy with Shadow Execution. arXiv e-prints, Article arXiv:1903.12254 (Mar 2019)."},{"key":"e_1_3_2_2_41_1","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems, Erika \u00c1brah\u00e1m and Catuscia Palamidessi (Eds.)","author":"Xu Lili","unstructured":"Lili Xu , Konstantinos Chatzikokolakis , and Huimin Lin . 2014. Metrics for Differential Privacy in Concurrent Systems . In Formal Techniques for Distributed Objects, Components, and Systems, Erika \u00c1brah\u00e1m and Catuscia Palamidessi (Eds.) . Springer Berlin Heidelberg , Berlin, Heidelberg , 199-215. Lili Xu, Konstantinos Chatzikokolakis, and Huimin Lin. 2014. Metrics for Differential Privacy in Concurrent Systems. In Formal Techniques for Distributed Objects, Components, and Systems, Erika \u00c1brah\u00e1m and Catuscia Palamidessi (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 199-215."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009884"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183713.3196921"}],"event":{"name":"PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Phoenix AZ USA","acronym":"PLDI '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314619","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314619","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:22Z","timestamp":1750204402000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314619"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,8]]},"references-count":43,"alternative-id":["10.1145\/3314221.3314619","10.1145\/3314221"],"URL":"https:\/\/doi.org\/10.1145\/3314221.3314619","relation":{},"subject":[],"published":{"date-parts":[[2019,6,8]]},"assertion":[{"value":"2019-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}