{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T21:11:09Z","timestamp":1743023469543,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031656293"},{"type":"electronic","value":"9783031656309"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T00:00:00Z","timestamp":1721865600000},"content-version":"vor","delay-in-days":206,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Envy-free cake-cutting protocols procedurally divide an infinitely divisible good among a set of agents so that no agent prefers another\u2019s allocation to their own. These protocols are highly complex and difficult to prove correct. Recently, Bertram, Levinson, and Hsu introduced a language called Slice for describing and verifying cake-cutting protocols. Slice programs can be translated to formulas encoding envy-freeness, which are solved by SMT. While Slice works well on smaller protocols, it has difficulty scaling to more complex cake-cutting protocols.<\/jats:p><jats:p>We improve Slice in two ways. First, we show any protocol execution in Slice can be replicated using piecewise uniform valuations. We then reduce Slice\u2019s constraint formulas to formulas within the theory of linear real arithmetic, showing that verifying envy-freeness is efficiently decidable. Second, we design and implement a linear type system which enforces that no two agents receive the same part of the good. We implement our methods and verify a range of challenging examples, including the first nontrivial four-agent protocol.<\/jats:p>","DOI":"10.1007\/978-3-031-65630-9_6","type":"book-chapter","created":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T22:01:56Z","timestamp":1721858516000},"page":"109-129","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Verifying Cake-Cutting, Faster"],"prefix":"10.1007","author":[{"given":"Noah","family":"Bertram","sequence":"first","affiliation":[]},{"given":"Tean","family":"Lai","sequence":"additional","affiliation":[]},{"given":"Justin","family":"Hsu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,25]]},"reference":[{"issue":"1","key":"6_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(93)90181-R","volume":"111","author":"S Abramsky","year":"1993","unstructured":"Abramsky, S.: Computational interpretations of linear logic. Theoret. Comput. Sci. 111(1), 3\u201357 (1993). https:\/\/doi.org\/10.1016\/0304-3975(93)90181-R","journal-title":"Theoret. Comput. Sci."},{"key":"6_CR2","doi-asserted-by":"publisher","unstructured":"Aziz, H., Mackenzie, S.: A discrete and bounded envy-free cake cutting protocol for four agents. In: ACM SIGACT Symposium on Theory of Computing (STOC), Cambridge, Massachusetts, pp. 454\u2013464 (2016).https:\/\/doi.org\/10.1145\/2897518.2897522","DOI":"10.1145\/2897518.2897522"},{"key":"6_CR3","unstructured":"Bertram, N., Lai, T., Hsu, J.: Verifying cake-cutting, faster (2024). https:\/\/arxiv.org\/abs\/2405.14068"},{"key":"6_CR4","doi-asserted-by":"publisher","unstructured":"Bertram, N., Levinson, A., Hsu, J.: Cutting the cake: a language for fair division. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Orlando, Florida (2023). https:\/\/doi.org\/10.1145\/3591293","DOI":"10.1145\/3591293"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-642-36946-9_10","volume-title":"Aliasing in Object-Oriented Programming. Types, Analysis and Verification","author":"J Boyland","year":"2013","unstructured":"Boyland, J.: Fractional permissions. In: Clarke, D., Noble, J., Wrigstad, T. (eds.) Aliasing in Object-Oriented Programming. Types, Analysis and Verification. LNCS, vol. 7850, pp. 270\u2013288. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36946-9_10"},{"key":"6_CR6","unstructured":"Brams, S.J., Jones, M.A., Klamler, C.: Better ways to cut a cake. Not. AMS 53(11), 1314\u20131321 (2006). https:\/\/www.ams.org\/cgi-bin\/notices\/"},{"key":"6_CR7","unstructured":"Geist, C.: Generating insights in social choice theory via computer-aided methods. Ph.D. thesis, Technical University Munich, Germany (2016). https:\/\/nbn-resolving.org\/urn:nbn:de:bvb:91-diss-20160906-1296898-1-8"},{"issue":"1","key":"6_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"JY Girard","year":"1987","unstructured":"Girard, J.Y.: Linear logic. Theoret. Comput. Sci. 50(1), 1\u2013101 (1987). https:\/\/doi.org\/10.1016\/0304-3975(87)90045-4","journal-title":"Theoret. Comput. Sci."},{"key":"6_CR9","doi-asserted-by":"publisher","unstructured":"Kurokawa, D., Lai, J., Procaccia, A.: How to cut a cake before the party ends. In: AAAI Conference on Artificial Intelligence, Bellevue, Washington (2013). https:\/\/doi.org\/10.1609\/aaai.v27i1.8629","DOI":"10.1609\/aaai.v27i1.8629"},{"issue":"1","key":"6_CR10","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/0304-3975(88)90100-4","volume":"59","author":"Y Lafont","year":"1988","unstructured":"Lafont, Y.: The linear abstract machine. Theoret. Comput. Sci. 59(1), 157\u2013180 (1988). https:\/\/doi.org\/10.1016\/0304-3975(88)90100-4","journal-title":"Theoret. Comput. Sci."},{"key":"6_CR11","doi-asserted-by":"publisher","unstructured":"Lester, M.M.: Cutting the cake into crumbs: verifying envy-free cake-cutting protocols using bounded integer arithmetic. In: Practical Aspects of Declarative Languages (PADL), London, England (2024). https:\/\/doi.org\/10.1007\/978-3-031-52038-9_7","DOI":"10.1007\/978-3-031-52038-9_7"},{"key":"6_CR12","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Budapest, Hungary (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"6_CR13","doi-asserted-by":"publisher","unstructured":"Nipkow, T.: Social choice theory in HOL. J. Autom. Reason. 43(3), 289\u2013304 (2009). https:\/\/doi.org\/10.1007\/S10817-009-9147-4","DOI":"10.1007\/S10817-009-9147-4"},{"key":"6_CR14","doi-asserted-by":"publisher","unstructured":"Procaccia, A.D.: Cake cutting algorithms. In: Brandt, F., Conitzer, V., Endriss, U., Lang, J., Procaccia, A.D. (eds.) Handbook of Computational Social Choice, pp. 311\u2013330, Cambridge University Press (2016). https:\/\/doi.org\/10.1017\/CBO9781107446984.014","DOI":"10.1017\/CBO9781107446984.014"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Robertson, J., Webb, W.: Cake-Cutting Algorithms: Be Fair If You Can. A K Peters\/CRC Press, Boca Raton (1998). https:\/\/doi.org\/10.1201\/9781439863855","DOI":"10.1201\/9781439863855"},{"issue":"1","key":"6_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2988232","volume":"13","author":"E Segal-Halevi","year":"2016","unstructured":"Segal-Halevi, E., Hassidim, A., Aumann, Y.: Waste makes haste: bounded time algorithms for envy-free cake cutting with free disposal. ACM Trans. Algorithms 13(1), 1\u201332 (2016). https:\/\/doi.org\/10.1145\/2988232","journal-title":"ACM Trans. Algorithms"},{"key":"6_CR17","unstructured":"Wadler, P.: Linear types can change the world! In: Programming Concepts and Methods, Sea of Galilee, Israel (1990)"},{"key":"6_CR18","doi-asserted-by":"publisher","unstructured":"Wadler, P.: Is there a use for linear logic? In: ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM), New Haven, Connecticut, USA (1991). https:\/\/doi.org\/10.1145\/115865.115894","DOI":"10.1145\/115865.115894"},{"key":"6_CR19","doi-asserted-by":"publisher","unstructured":"Walker, D.: Substructural type systems. In: Pierce, B.C. (ed.) Advanced Topics in Types and Programming Languages. The MIT Press (2004). https:\/\/doi.org\/10.7551\/mitpress\/1104.003.0003","DOI":"10.7551\/mitpress\/1104.003.0003"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65630-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T22:03:00Z","timestamp":1721858580000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65630-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656293","9783031656309"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65630-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"25 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","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":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}