{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T23:46:11Z","timestamp":1762299971169,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030945824"},{"type":"electronic","value":"9783030945831"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-030-94583-1_9","type":"book-chapter","created":{"date-parts":[[2022,1,13]],"date-time":"2022-01-13T22:02:34Z","timestamp":1642111354000},"page":"174-196","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Verifying Pufferfish Privacy in\u00a0Hidden Markov Models"],"prefix":"10.1007","author":[{"given":"Depeng","family":"Liu","sequence":"first","affiliation":[]},{"given":"Bow-Yaw","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,1,14]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A., Hsu, J.: Synthesizing coupling proofs of differential privacy. Proc. ACM Program. Lang. 2(POPL), 1\u201330 (2017)","DOI":"10.1145\/3158146"},{"key":"9_CR2","unstructured":"Apple: About privacy and location services in IOS and IPADOS (2020). https:\/\/support.apple.com\/en-us\/HT203033\/. Accessed 9 Sept 2021"},{"key":"9_CR3","doi-asserted-by":"publisher","unstructured":"Barthe, G., Chadha, R., Jagannath, V., Sistla, A., Viswanathan, M.: Deciding differential privacy for programs with finite inputs and outputs, pp. 141\u2013154 (2020). https:\/\/doi.org\/10.1145\/3373718.3394796","DOI":"10.1145\/3373718.3394796"},{"key":"9_CR4","unstructured":"Barthe, G., Chadha, R., Jagannath, V., Sistla, A.P., Viswanathan, M.: Automated methods for checking differential privacy. CoRR abs\/1910.04137 (2019). http:\/\/arxiv.org\/abs\/1910.04137"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gaboardi, M., Gr\u00e9goire, B., Hsu, J., Strub, P.Y.: Proving differential privacy via probabilistic couplings (2016)","DOI":"10.1145\/2933575.2934554"},{"issue":"1","key":"9_CR6","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1145\/2893582.2893591","volume":"3","author":"G Barthe","year":"2016","unstructured":"Barthe, G., Gaboardi, M., Hsu, J., Pierce, B.: Programming language techniques for differential privacy. ACM SIGLOG News 3(1), 34\u201353 (2016). https:\/\/doi.org\/10.1145\/2893582.2893591","journal-title":"ACM SIGLOG News"},{"key":"9_CR7","doi-asserted-by":"publisher","unstructured":"Barthe, G., K\u00f6pf, B., Olmedo, F., Zanella B\u00e9guelin, S.: Probabilistic relational reasoning for differential privacy. In: POPL \u201912, pp. 97\u2013110 (2012). https:\/\/doi.org\/10.1145\/2103656.2103670","DOI":"10.1145\/2103656.2103670"},{"issue":"1","key":"9_CR8","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/2103621.2103670","volume":"47","author":"G Barthe","year":"2012","unstructured":"Barthe, G., K\u00f6pf, B., Olmedo, F., Zanella B\u00e9guelin, S.: Probabilistic relational reasoning for differential privacy. SIGPLAN Not. 47(1), 97\u2013110 (2012). https:\/\/doi.org\/10.1145\/2103621.2103670","journal-title":"SIGPLAN Not."},{"key":"9_CR9","doi-asserted-by":"publisher","unstructured":"Bichsel, B., Gehr, T., Drachsler-Cohen, D., Tsankov, P., Vechev, M.: Dp-finder: finding differential privacy violations by sampling and optimization, pp. 508\u2013524 (2018). https:\/\/doi.org\/10.1145\/3243734.3243863","DOI":"10.1145\/3243734.3243863"},{"key":"9_CR10","doi-asserted-by":"publisher","unstructured":"Bichsel, B., Steffen, S., Bogunovic, I., Vechev, M.: DP-sniper: black-box discovery of differential privacy violations using classifiers. In: SP\u201921, pp. 391\u2013409 (2021). https:\/\/doi.org\/10.1109\/SP40001.2021.00081","DOI":"10.1109\/SP40001.2021.00081"},{"key":"9_CR11","unstructured":"Chen, Y., Machanavajjhala, A.: On the privacy properties of variants on the sparse vector technique. CoRR abs\/1508.07306 (2015). http:\/\/arxiv.org\/abs\/1508.07306"},{"key":"9_CR12","doi-asserted-by":"publisher","unstructured":"Chistikov, D., Kiefer, S., Murawski, A.S., Purser, D.: The Big-O problem for labelled markov chains and weighted automata. In: CONCUR 2020. Leibniz International Proceedings in Informatics (LIPIcs), vol. 171, pp. 41:1\u201341:19 (2020). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2020.41","DOI":"10.4230\/LIPIcs.CONCUR.2020.41"},{"key":"9_CR13","unstructured":"Ding, B., Kulkarni, J., Yekhanin, S.: Collecting telemetry data privately. In: NIPS\u201917, pp. 3574\u20133583 (2017)"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Ding, Z., Wang, Y., Wang, G., Zhang, D., Kifer, D.: Detecting violations of differential privacy. In: Backes, M., Wang, X. (eds.) CCS, pp. 475\u2013489 (2018)","DOI":"10.1145\/3243734.3243818"},{"issue":"2","key":"9_CR15","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/261320.261324","volume":"31","author":"A Dolzmann","year":"1997","unstructured":"Dolzmann, A., Sturm, T.: REDLOG: computer algebra meets computer logic. SIGSAM Bull. 31(2), 2\u20139 (1997). https:\/\/doi.org\/10.1145\/261320.261324","journal-title":"SIGSAM Bull."},{"issue":"3\u20134","key":"9_CR16","first-page":"211","volume":"9","author":"C Dwork","year":"2014","unstructured":"Dwork, C., Roth, A.: The algorithmic foundations of differential privacy. Found. Trends Theoret. Comput. Sci. 9(3\u20134), 211\u2013407 (2014)","journal-title":"Found. Trends Theoret. Comput. Sci."},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11787006_1","volume-title":"Automata, Languages and Programming","author":"C Dwork","year":"2006","unstructured":"Dwork, C.: Differential privacy. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 1\u201312. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11787006_1"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Farina, G.P., Chong, S., Gaboardi, M.: Coupled relational symbolic execution for differential privacy. In: Programming Languages and Systems, pp. 207\u2013233 (2021)","DOI":"10.1007\/978-3-030-72019-3_8"},{"key":"9_CR19","doi-asserted-by":"publisher","unstructured":"Gaboardi, M., Nissim, K., Purser, D.: The complexity of verifying loop-free programs as differentially private. In: ICALP 2020. Leibniz International Proceedings in Informatics (LIPIcs), vol. 168, pp. 129:1\u2013129:17 (2020). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2020.129","DOI":"10.4230\/LIPIcs.ICALP.2020.129"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Ghosh, A., Roughgarden, T., Sundararajan, M.: Universally utility-maximizing privacy mechanisms. In: STOC, pp. 351\u2013360. ACM, New York (2009)","DOI":"10.1145\/1536414.1536464"},{"issue":"6","key":"9_CR21","doi-asserted-by":"publisher","first-page":"1673","DOI":"10.1137\/09076828X","volume":"41","author":"A Ghosh","year":"2012","unstructured":"Ghosh, A., Roughgarden, T., Sundararajan, M.: Universally utility-maximizing privacy mechanisms. SIAM J. Comput. 41(6), 1673\u20131693 (2012)","journal-title":"SIAM J. Comput."},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Kifer, D., Machanavajjhala, A.: No free lunch in data privacy. In: SIGMOD, pp. 193\u2013204 (2011)","DOI":"10.1145\/1989323.1989345"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Kifer, D., Machanavajjhala, A.: Pufferfish: a framework for mathematical privacy definitions. ACM Trans. Database Syst. 39(1), 3:1\u20133:36 (2014)","DOI":"10.1145\/2514689"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/978-3-030-02768-1_21","volume-title":"Programming Languages and Systems","author":"D Liu","year":"2018","unstructured":"Liu, D., Wang, B.-Y., Zhang, L.: Model checking differentially private properties. In: Ryu, S. (ed.) APLAS 2018. LNCS, vol. 11275, pp. 394\u2013414. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02768-1_21"},{"key":"9_CR25","unstructured":"Liu, D., Wang, B., Zhang, L.: Verifying pufferfish privacy in hidden Markov models. CoRR abs\/2008.01704 (2020). https:\/\/arxiv.org\/abs\/2008.01704"},{"key":"9_CR26","doi-asserted-by":"publisher","unstructured":"Lyu, M., Su, D., Li, N.: Understanding the sparse vector technique for differential privacy. Proc. VLDB Endow. 10(6), 637\u2013648 (2017). https:\/\/doi.org\/10.14778\/3055330.3055331","DOI":"10.14778\/3055330.3055331"},{"key":"9_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-34175-6_1","volume-title":"Programming Languages and Systems","author":"A McIver","year":"2019","unstructured":"McIver, A., Morgan, C.: Proving that programs are differentially private. In: Lin, A.W. (ed.) APLAS 2019. LNCS, vol. 11893, pp. 3\u201318. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-34175-6_1"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Mironov, I.: On significance of the least significant bits for differential privacy. In: CCS\u201912, pp. 650\u2013661 (2012)","DOI":"10.1145\/2382196.2382264"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"3","key":"9_CR30","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1287\/moor.12.3.441","volume":"12","author":"CH Papadimitriou","year":"1987","unstructured":"Papadimitriou, C.H., Tsitsiklis, J.N.: The complexity of Markov decision processes. Math. Oper. Res. 12(3), 441\u2013450 (1987)","journal-title":"Math. Oper. Res."},{"issue":"2","key":"9_CR31","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1109\/5.18626","volume":"77","author":"LR Rabiner","year":"1989","unstructured":"Rabiner, L.R.: A tutorial on hidden Markov models and selected applications in speech recognition. Proc. IEEE 77(2), 257\u2013286 (1989)","journal-title":"Proc. IEEE"},{"key":"9_CR32","doi-asserted-by":"publisher","unstructured":"Wang, Y., Ding, Z., Kifer, D., Zhang, D.: CheckDP: an automated and integrated approach for proving differential privacy or finding precise counterexamples. In: CCS \u201920, pp. 919\u2013938 (2020). https:\/\/doi.org\/10.1145\/3372297.3417282","DOI":"10.1145\/3372297.3417282"},{"key":"9_CR33","doi-asserted-by":"crossref","unstructured":"Wang, Y., Ding, Z., Wang, G., Kifer, D., Zhang, D.: Proving differential privacy with shadow execution. In: PLDI\u201919, pp. 655\u2013669 (2019)","DOI":"10.1145\/3314221.3314619"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"Zhang, D., Kifer, D.: LightDP: towards automating differential privacy proofs. In: POPL\u201917, vol. 52, pp. 888\u2013901 (2017)","DOI":"10.1145\/3093333.3009884"},{"key":"9_CR35","doi-asserted-by":"publisher","unstructured":"Zhang, H., Roth, E., Haeberlen, A., Pierce, B.C., Roth, A.: Testing differential privacy with dual interpreters. Proc. ACM Program. Lang. 4(OOPSLA) (2020). https:\/\/doi.org\/10.1145\/3428233","DOI":"10.1145\/3428233"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-94583-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,14]],"date-time":"2022-01-14T00:05:04Z","timestamp":1642118704000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-94583-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030945824","9783030945831"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-94583-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"14 January 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Philadelphia, PA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 January 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl22.sigplan.org\/home\/VMCAI-2022","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"63","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"37% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}