{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T06:28:15Z","timestamp":1750746495783,"version":"3.37.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319961446"},{"type":"electronic","value":"9783319961453"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96145-3_18","type":"book-chapter","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T18:25:55Z","timestamp":1532111155000},"page":"327-346","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Constraint-Based Synthesis of Coupling Proofs"],"prefix":"10.1007","author":[{"given":"Aws","family":"Albarghouthi","sequence":"first","affiliation":[]},{"given":"Justin","family":"Hsu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"issue":"POPL","key":"18_CR1","first-page":"58:1","volume":"2","author":"A Albarghouthi","year":"2018","unstructured":"Albarghouthi, A., Hsu, J.: Synthesizing coupling proofs of differential privacy. Proc. ACM Programm. Lang. 2(POPL), 58:1\u201358:30 (2018). http:\/\/doi.acm.org\/10.1145\/3158146","journal-title":"Proc. ACM Programm. Lang."},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Bodik, R., Juniwal, G., Martin, M.M., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design (FMCAD), Portland, Oregon, pp. 1\u20138. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"18_CR3","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-21437-0_17","volume-title":"FM 2011: Formal Methods","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 200\u2013214. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_17"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Barthe, G., Espitau, T., Gaboardi, M., Gr\u00e9goire, B., Hsu, J., Strub, P.Y.: A program logic for probabilistic programs. In: European Symposium on Programming (ESOP), Thessaloniki, Greece (2018, to appear). https:\/\/justinh.su\/files\/papers\/ellora.pdf","DOI":"10.1007\/978-3-319-89884-1_5"},{"key":"18_CR6","unstructured":"Barthe, G., Espitau, T., Gr\u00e9goire, B., Hsu, J., Strub, P.Y.: Proving uniformity and independence by self-composition and coupling. In: International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Maun, Botswana. EPiC Series in Computing, vol. 46, pp. 385\u2013403 (2017). https:\/\/arxiv.org\/abs\/1701.06477"},{"issue":"POPL","key":"18_CR7","first-page":"57:1","volume":"2","author":"G Barthe","year":"2018","unstructured":"Barthe, G., Espitau, T., Gr\u00e9goire, B., Hsu, J., Strub, P.: Proving expected sensitivity of probabilistic programs. Proc. ACM Programm. Lang. 2(POPL), 57:1\u201357:29 (2018). http:\/\/doi.acm.org\/10.1145\/3158145","journal-title":"Proc. ACM Programm. Lang."},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Barthe, G., Fong, N., Gaboardi, M., Gr\u00e9goire, B., Hsu, J., Strub, P.Y.: Advanced probabilistic couplings for differential privacy. In: ACM SIGSAC Conference on Computer and Communications Security (CCS), Vienna, Austria (2016). https:\/\/arxiv.org\/abs\/1606.07143","DOI":"10.1145\/2976749.2978391"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Barthe, G., Fournet, C., Gr\u00e9goire, B., Strub, P.Y., Swamy, N., Zanella-B\u00e9guelin, S.: Probabilistic relational verification for cryptographic implementations. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), San Diego, California, pp. 193\u2013206 (2014). https:\/\/research.microsoft.com\/en-us\/um\/people\/nswamy\/papers\/rfstar.pdf","DOI":"10.1145\/2535838.2535847"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gaboardi, M., Gr\u00e9goire, B., Hsu, J., Strub, P.Y.: Proving differential privacy via probabilistic couplings. In: IEEE Symposium on Logic in Computer Science (LICS), New York, pp. 749\u2013758 (2016), http:\/\/arxiv.org\/abs\/1601.05047","DOI":"10.1145\/2933575.2934554"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., Hsu, J., Strub, P.Y.: Coupling proofs are probabilistic product programs. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Paris, France, pp. 161\u2013174 (2017). http:\/\/arxiv.org\/abs\/1607.03455","DOI":"10.1145\/3009837.3009896"},{"issue":"3","key":"18_CR12","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1145\/2492061","volume":"35","author":"G Barthe","year":"2013","unstructured":"Barthe, G., K\u00f6pf, B., Olmedo, F., Zanella-B\u00e9guelin, S.: Probabilistic relational reasoning for differential privacy. ACM Trans. Programm. Lang. Syst. 35(3), 9 (2013). http:\/\/software.imdea.org\/~bkoepf\/papers\/toplas13.pdf","journal-title":"ACM Trans. Programm. Lang. Syst."},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Beyene, T., Chaudhuri, S., Popeea, C., Rybalchenko, A.: A constraint-based approach to solving games on infinite graphs. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), San Diego, California, pp. 221\u2013233 (2014)","DOI":"10.1145\/2535838.2535860"},{"issue":"1","key":"18_CR14","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/j.tcs.2007.02.040","volume":"379","author":"R Chadha","year":"2007","unstructured":"Chadha, R., Cruz-Filipe, L., Mateus, P., Sernadas, A.: Reasoning about probabilistic sequential programs. Theor. Comput. Sci. 379(1), 142\u2013165 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-41528-4_1","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2016","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through Positivstellensatz\u2019s. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 3\u201322. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_1"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Novotn\u00fd, P., Hasheminezhad, R.: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Saint Petersburg, Florida, pp. 327\u2013342 (2016). https:\/\/doi.acm.org\/10.1145\/2837614.2837639","DOI":"10.1145\/2837614.2837639"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Novotn\u00fd, P., \u017dikeli\u0107, \u0110.: Stochastic invariants for probabilistic termination. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Paris, France, pp. 145\u2013160 (2017). https:\/\/doi.acm.org\/10.1145\/3009837.3009873","DOI":"10.1145\/3009837.3009873"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"key":"18_CR19","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 Moura de","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"},{"key":"18_CR20","volume-title":"An Introduction to Probability Theory and Its Applications","author":"W Feller","year":"1968","unstructured":"Feller, W.: An Introduction to Probability Theory and Its Applications, vol. 1, 3rd edn. Wiley, Hoboken (1968)","edition":"3"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-21455-4_3","volume-title":"Formal Methods for Eternal Networked Software Systems","author":"V Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53\u2013113. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21455-4_3"},{"key":"18_CR22","unstructured":"den Hartog, J.: Probabilistic extensions of semantical models. Ph.D. thesis, Vrije Universiteit Amsterdam (2002)"},{"key":"18_CR23","unstructured":"Hsu, J.: Probabilistic Couplings for Probabilistic Reasoning. Ph.D. thesis, University of Pennsylvania (2017). https:\/\/arxiv.org\/abs\/1710.09951"},{"issue":"3","key":"18_CR24","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1016\/0022-0000(81)90036-2","volume":"22","author":"D Kozen","year":"1981","unstructured":"Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328\u2013350 (1981). https:\/\/www.sciencedirect.com\/science\/article\/pii\/0022000081900362","journal-title":"J. Comput. Syst. Sci."},{"issue":"3","key":"18_CR25","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1145\/229542.229547","volume":"18","author":"C Morgan","year":"1996","unstructured":"Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Trans. Programm. Lang. Syst. 18(3), 325\u2013353 (1996). dl.acm.org\/ft_gateway.cfm?id=229547","journal-title":"ACM Trans. Programm. Lang. Syst."},{"key":"18_CR26","doi-asserted-by":"crossref","unstructured":"Rand, R., Zdancewic, S.: VPHL: a verified partial-correctness logic for probabilistic programs. In: Conference on the Mathematical Foundations of Programming Semantics (MFPS), Nijmegen, The Netherlands (2015)","DOI":"10.1016\/j.entcs.2015.12.021"},{"key":"18_CR27","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: International Conference on Architectural Support for Programming Langauages and Operating Systems (ASPLOS), San Jose, California, pp. 404\u2013415 (2006). http:\/\/doi.acm.org\/10.1145\/1168857.1168907","DOI":"10.1145\/1168857.1168907"},{"key":"18_CR28","doi-asserted-by":"crossref","unstructured":"Strassen, V.: The existence of probability measures with given marginals. Annals Math. Stat. 423\u2013439 (1965). https:\/\/projecteuclid.org\/euclid.aoms\/1177700153","DOI":"10.1214\/aoms\/1177700153"},{"key":"18_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-540-68237-0_5","volume-title":"FM 2008: Formal Methods","author":"A Zaks","year":"2008","unstructured":"Zaks, A., Pnueli, A.: CoVaC: compiler validation by program analysis of the cross-product. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 35\u201351. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68237-0_5"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96145-3_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T23:32:20Z","timestamp":1571614340000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96145-3_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319961446","9783319961453"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96145-3_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}