{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,7]],"date-time":"2025-12-07T16:02:52Z","timestamp":1765123372001,"version":"3.40.4"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031908965"},{"type":"electronic","value":"9783031908972"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This work is devoted to formal reasoning on relational properties of probabilistic imperative programs. Relational properties are properties which relate the execution of two programs (possibly the same one) on two initial memories. We aim at extending the algebraic approach of Kleene Algebras with Tests (KAT) to relational properties of probabilistic programs. For that we consider the approach of Guarded Kleene Algebras with Tests (GKAT), which can be used for representing probabilistic programs, and define a relational version of it, called Bi-guarded Kleene Algebras with Tests (BiGKAT) together with a semantics. We show that the setting of BiGKAT is expressive enough to encode a finitary version of probabilistic Relational Hoare Logic (pRHL) (without the While rule), a program logic that has been introduced in the literature for the verification of relational properties of probabilistic programs. We also discuss the additional expressivity brought by BiGKAT.<\/jats:p>","DOI":"10.1007\/978-3-031-90897-2_12","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:18:08Z","timestamp":1746001088000},"page":"243-264","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["BiGKAT: An Algebraic Framework for Relational Verification of Probabilistic Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1180-0620","authenticated-orcid":false,"given":"Leandro","family":"Gomes","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0002-9364-1140","authenticated-orcid":false,"given":"Patrick","family":"Baillot","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5235-7066","authenticated-orcid":false,"given":"Marco","family":"Gaboardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","unstructured":"Timos Antonopoulos, Eric Koskinen, Ton\u00a0Chanh Le, Ramana Nagasamudram, David\u00a0A. Naumann, and Minh Ngo. An algebra of alignment for relational verification. Proc. ACM Program. Lang., 7(POPL):573\u2013603, 2023. https:\/\/doi.org\/10.1145\/3571213.","DOI":"10.1145\/3571213"},{"key":"12_CR2","doi-asserted-by":"publisher","unstructured":"Martin Avanzini, Gilles Barthe, Benjamin Gr\u00e9goire, Georg Moser, and Gabriele Vanoni. Hopping proofs of expectation-based properties: Applications to skiplists and security proofs. Proc. ACM Program. Lang., 8(OOPSLA1):784\u2013809, 2024. https:\/\/doi.org\/10.1145\/3649839.","DOI":"10.1145\/3649839"},{"key":"12_CR3","doi-asserted-by":"publisher","unstructured":"Gilles Barthe, Fran\u00e7ois Dupressoir, Benjamin Gr\u00e9goire, C\u00e9sar Kunz, Benedikt Schmidt, and Pierre-Yves Strub. Easycrypt: A tutorial. In Alessandro Aldini, Javier L\u00f3pez, and Fabio Martinelli, editors, Foundations of Security Analysis and Design VII - FOSAD 2012\/2013 Tutorial Lectures, volume 8604 of Lecture Notes in Computer Science, pages 146\u2013166. Springer, 2013. https:\/\/doi.org\/10.1007\/978-3-319-10082-1_6.","DOI":"10.1007\/978-3-319-10082-1_6"},{"key":"12_CR4","doi-asserted-by":"publisher","unstructured":"Gilles Barthe, Marco Gaboardi, Benjamin Gr\u00e9goire, Justin Hsu, and Pierre-Yves Strub. A program logic for union bounds. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume\u00a055 of LIPIcs, pages 107:1\u2013107:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2016. https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2016.107.","DOI":"10.4230\/LIPIcs.ICALP.2016.107"},{"key":"12_CR5","doi-asserted-by":"publisher","unstructured":"Gilles Barthe, Marco Gaboardi, Justin Hsu, and Benjamin\u00a0C. Pierce. Programming language techniques for differential privacy. ACM SIGLOG News, 3(1):34\u201353, 2016. https:\/\/doi.org\/10.1145\/2893582.2893591.","DOI":"10.1145\/2893582.2893591"},{"key":"12_CR6","doi-asserted-by":"publisher","unstructured":"Gilles Barthe, Benjamin Gr\u00e9goire, and Santiago\u00a0Zanella B\u00e9guelin. Formal certification of code-based cryptographic proofs. In Zhong Shao and Benjamin\u00a0C. Pierce, editors, Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, pages 90\u2013101. ACM, 2009. https:\/\/doi.org\/10.1145\/1480881.1480894.","DOI":"10.1145\/1480881.1480894"},{"key":"12_CR7","doi-asserted-by":"publisher","unstructured":"Gilles Barthe, Benjamin Gr\u00e9goire, Justin Hsu, and Pierre-Yves Strub. Coupling proofs are probabilistic product programs. In Giuseppe Castagna and Andrew\u00a0D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 161\u2013174. ACM, 2017. https:\/\/doi.org\/10.1145\/3009837.3009896.","DOI":"10.1145\/3009837.3009896"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Gilles Barthe, Boris K\u00f6pf, Federico Olmedo, and Santiago\u00a0Zanella B\u00e9guelin. Probabilistic relational reasoning for differential privacy. ACM Trans. Program. Lang. Syst., 35(3):9:1\u20139:49, 2013. https:\/\/doi.org\/10.1145\/2492061.","DOI":"10.1145\/2492061"},{"key":"12_CR9","doi-asserted-by":"publisher","unstructured":"Santiago\u00a0Zanella B\u00e9guelin, Gilles Barthe, Benjamin Gr\u00e9goire, and Federico Olmedo. Formally certifying the security of digital signature schemes. In 30th IEEE Symposium on Security and Privacy (S &P 2009), 17-20 May 2009, Oakland, California, USA, pages 237\u2013250. IEEE Computer Society, 2009. https:\/\/doi.org\/10.1109\/SP.2009.17.","DOI":"10.1109\/SP.2009.17"},{"key":"12_CR10","doi-asserted-by":"publisher","unstructured":"Nick Benton. Simple relational correctness proofs for static analyses and program transformations. In Neil\u00a0D. Jones and Xavier Leroy, editors, Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004, pages 14\u201325. ACM, 2004. https:\/\/doi.org\/10.1145\/964001.964003.","DOI":"10.1145\/964001.964003"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Raven Beutner. Automated software verification of hyperliveness. In Bernd Finkbeiner and Laura Kov\u00e1cs, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 196\u2013216, Cham, 2024. Springer Nature Switzerland.","DOI":"10.1007\/978-3-031-57249-4_10"},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Filippo Bonchi and Damien Pous. Checking NFA equivalence with bisimulations up to congruence. In Roberto Giacobazzi and Radhia Cousot, editors, The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913, Rome, Italy - January 23 - 25, 2013, pages 457\u2013468. ACM, 2013. https:\/\/doi.org\/10.1145\/2429069.2429124.","DOI":"10.1145\/2429069.2429124"},{"key":"12_CR13","doi-asserted-by":"publisher","unstructured":"Robert Dickerson, Qianchuan Ye, Michael\u00a0K. Zhang, and Benjamin Delaware. RHLE: Modular deductive verification of relational forall exists properties. In Ilya Sergey, editor, Programming Languages and Systems - 20th Asian Symposium, APLAS 2022, Auckland, New Zealand, December 5, 2022, Proceedings, volume 13658 of Lecture Notes in Computer Science, pages 67\u201387. Springer, 2022. https:\/\/doi.org\/10.1007\/978-3-031-21037-2_4.","DOI":"10.1007\/978-3-031-21037-2_4"},{"key":"12_CR14","unstructured":"Leandro Gomes, Patrick Baillot, and Marco Gaboardi. A Kleene algebra with tests for union bound reasoning about probabilistic programs. In 33rd EACSL Annual Conference on Computer Science Logic, CSL 2025, volume 326. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2025. to appear. URL: https:\/\/hal.science\/hal-04196675."},{"key":"12_CR15","unstructured":"Leandro Gomes, Patrick Baillot, and Marco Gaboardi. BiGKAT: an algebraic framework for relational verification of probabilistic programs. Technical report, 2025. URL: https:\/\/hal.science\/hal-04017128."},{"key":"12_CR16","doi-asserted-by":"publisher","unstructured":"D.\u00a0Kozen. Kleene algebra with tests. ACM Trans. on Prog. Lang. and Systems, 19(3):427\u2013443, 1997. https:\/\/doi.org\/10.1145\/256167.256195.","DOI":"10.1145\/256167.256195"},{"key":"12_CR17","doi-asserted-by":"publisher","unstructured":"D.\u00a0Kozen. On Hoare logic and Kleene algebra with tests. ACM Trans. on Comp. Logic, 1(212):1\u201314, 2000. URL: http:\/\/dl.acm.org\/citation.cfm?id=343378, https:\/\/doi.org\/10.1109\/LICS.1999.782610.","DOI":"10.1109\/LICS.1999.782610"},{"key":"12_CR18","doi-asserted-by":"publisher","unstructured":"Dexter Kozen. Kleene algebra with tests and commutativity conditions. In Tiziana Margaria and Bernhard Steffen, editors, Tools and Algorithms for Construction and Analysis of Systems, Second International Workshop, TACAS \u201996, Passau, Germany, March 27-29, 1996, Proceedings, volume 1055 of Lecture Notes in Computer Science, pages 14\u201333. Springer, 1996. https:\/\/doi.org\/10.1007\/3-540-61042-1_35.","DOI":"10.1007\/3-540-61042-1_35"},{"key":"12_CR19","doi-asserted-by":"publisher","unstructured":"Damien Pous. Kleene algebra with tests and coq tools for while programs. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, volume 7998 of Lecture Notes in Computer Science, pages 180\u2013196. Springer, 2013. https:\/\/doi.org\/10.1007\/978-3-642-39634-2_15.","DOI":"10.1007\/978-3-642-39634-2_15"},{"key":"12_CR20","doi-asserted-by":"publisher","unstructured":"Wojciech Rozowski, Tobias Kapp\u00e9, Dexter Kozen, Todd Schmid, and Alexandra Silva. Probabilistic guarded KAT modulo bisimilarity: Completeness and complexity. In Kousha Etessami, Uriel Feige, and Gabriele Puppis, editors, 50th International Colloquium on Automata, Languages, and Programming, ICALP 2023, July 10-14, 2023, Paderborn, Germany, volume 261 of LIPIcs, pages 136:1\u2013136:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2023. https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2023.136.","DOI":"10.4230\/LIPIcs.ICALP.2023.136"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Todd Schmid, Tobias Kapp\u00e9, Dexter Kozen, and Alexandra Silva. Guarded Kleene algebra with tests: Coequations, coinduction, and completeness. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), volume 198 of LIPIcs, pages 142:1\u2013142:14. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2021. https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2021.142.","DOI":"10.4230\/LIPIcs.ICALP.2021.142"},{"key":"12_CR22","doi-asserted-by":"publisher","unstructured":"Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kapp\u00e9, Dexter Kozen, and Alexandra Silva. Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time. Proc. ACM Program. Lang., 4(POPL):61:1\u201361:28, 2020. https:\/\/doi.org\/10.1145\/3371129.","DOI":"10.1145\/3371129"},{"key":"12_CR23","doi-asserted-by":"publisher","unstructured":"Daniele Varacca and Glynn Winskel. Distributing probability over non-determinism. Math. Struct. Comput. Sci., 16(1):87\u2013113, 2006. https:\/\/doi.org\/10.1017\/S0960129505005074.","DOI":"10.1017\/S0960129505005074"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90897-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:18:10Z","timestamp":1746001090000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90897-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031908965","9783031908972"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90897-2_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/fossacs\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}