{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T21:44:46Z","timestamp":1742939086265,"version":"3.40.3"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031520372"},{"type":"electronic","value":"9783031520389"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-52038-9_7","type":"book-chapter","created":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T06:02:40Z","timestamp":1704780160000},"page":"100-115","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Cutting the Cake into Crumbs: Verifying Envy-Free Cake-Cutting Protocols Using Bounded Integer Arithmetic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2323-1771","authenticated-orcid":false,"given":"Martin Mariusz","family":"Lester","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,1,10]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"Audemard, G., Lecoutre, C., Lonca, E.: Proceedings of the 2022 XCSP3 competition. CoRR abs\/2209.00917 (2022). https:\/\/doi.org\/10.48550\/arXiv.2209.00917","DOI":"10.48550\/arXiv.2209.00917"},{"key":"7_CR2","doi-asserted-by":"publisher","unstructured":"Aumann, Y., Lang, J., Procaccia, A.D.: Fair division (dagstuhl seminar 16232). Dagstuhl Rep. 6(6), 10\u201325 (2016). https:\/\/doi.org\/10.4230\/DagRep.6.6.10","DOI":"10.4230\/DagRep.6.6.10"},{"key":"7_CR3","doi-asserted-by":"publisher","unstructured":"Aziz, H., Mackenzie, S.: A discrete and bounded envy-free cake cutting protocol for any number of agents. In: Dinur, I. (ed.) IEEE 57th Annual Symposium on Foundations of Computer Science, FOCS 2016, 9\u201311 October 2016, Hyatt Regency, New Brunswick, New Jersey, USA, pp. 416\u2013427. IEEE Computer Society (2016). https:\/\/doi.org\/10.1109\/FOCS.2016.52","DOI":"10.1109\/FOCS.2016.52"},{"key":"7_CR4","doi-asserted-by":"publisher","unstructured":"Aziz, H., Mackenzie, S.: A bounded and envy-free cake cutting algorithm. Commun. ACM 63(4), 119\u2013126 (2020). https:\/\/doi.org\/10.1145\/3382129","DOI":"10.1145\/3382129"},{"key":"7_CR5","doi-asserted-by":"publisher","unstructured":"Bertram, N., Levinson, A., Hsu, J.: Cutting the cake: a language for fair division. CoRR abs\/2304.04642 (2023). https:\/\/doi.org\/10.48550\/arXiv.2304.04642","DOI":"10.48550\/arXiv.2304.04642"},{"key":"7_CR6","unstructured":"Biere, A., Fleury, M.: Gimsatul, IsaSAT and Kissat entering the SAT competition 2022. In: Balyo, T., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proceedings of the SAT Competition 2022 - Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2022-1, pp. 10\u201311. University of Helsinki (2022). http:\/\/hdl.handle.net\/10138\/359079"},{"key":"7_CR7","unstructured":"Brams, S.J., Pruhs, K., Woeginger, G.J. (eds.): Fair Division, 24.06.\u201329.06.2007, Dagstuhl Seminar Proceedings, vol. 07261. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany (2007). http:\/\/drops.dagstuhl.de\/portals\/07261\/"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-319-24318-4_26","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"F Corzilius","year":"2015","unstructured":"Corzilius, F., Kremer, G., Junges, S., Schupp, S., \u00c1brah\u00e1m, E.: SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 360\u2013368. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_26"},{"key":"7_CR10","unstructured":"Klarreich, E.: How to cut cake fairly and finally eat it too. Quanta Magazine, October 2016. https:\/\/www.quantamagazine.org\/new-algorithm-solves-cake-cutting-problem-20161006\/"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C bounded model checker. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_26"},{"key":"7_CR12","doi-asserted-by":"publisher","unstructured":"Lester, M.M.: CoPTIC: constraint programming translated into C. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2023. LNCS, vol. 13994, pp. 173\u2013191. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_13","DOI":"10.1007\/978-3-031-30820-8_13"},{"key":"7_CR13","doi-asserted-by":"publisher","unstructured":"Lester, M.M.: Crumbs: A DSL for Verifying Envy-Free Cake-Cutting Protocols using Bounded Integer Arithmetic, January 2024. https:\/\/doi.org\/10.5281\/zenodo.10205142","DOI":"10.5281\/zenodo.10205142"},{"key":"7_CR14","unstructured":"Manthey, N.: Solving summle.net with SAT. In: Balyo, T., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proceedings of the SAT Competition 2022 - Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2022-1, pp. 70\u201371. University of Helsinki (2022). http:\/\/hdl.handle.net\/10138\/359079"},{"key":"7_CR15","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"},{"key":"7_CR16","doi-asserted-by":"publisher","unstructured":"Procaccia, A.D.: Cake cutting: not just child\u2019s play. Commun. ACM 56(7), 78\u201387 (2013). https:\/\/doi.org\/10.1145\/2483852.2483870","DOI":"10.1145\/2483852.2483870"}],"container-title":["Lecture Notes in Computer Science","Practical Aspects of Declarative Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-52038-9_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T06:06:21Z","timestamp":1704780381000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-52038-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031520372","9783031520389"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-52038-9_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"10 January 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"PADL","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Practical Aspects of Declarative Languages","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"London","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 January 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"padl2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl24.sigplan.org\/home\/PADL-2024","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"HotCRP","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"25","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":"13","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":"52% - 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":"4","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":"4","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)"}}]}}