{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:15:21Z","timestamp":1775873721856,"version":"3.50.1"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2024,1,15]],"date-time":"2024-01-15T00:00:00Z","timestamp":1705276800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"German Federal Ministry of Education and Research together with the Hessen State Ministry for Higher Education (ATHENE), the German Research Foundation","award":["SFB 1053"],"award-info":[{"award-number":["SFB 1053"]}]},{"name":"German Federal Ministry for Economic Affairs and Climate Action project SafeFBDC","award":["01MK21002K"],"award-info":[{"award-number":["01MK21002K"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2024,3,31]]},"abstract":"<jats:p>Local-first software manages and processes private data locally while still enabling collaboration between multiple parties connected via partially unreliable networks. Such software typically involves interactions with users and the execution environment (the outside world). The unpredictability of such interactions paired with their decentralized nature make reasoning about the correctness of local-first software a challenging endeavor. Yet, existing solutions to develop local-first software do not provide support for automated safety guarantees and instead expect developers to reason about concurrent interactions in an environment with unreliable network conditions.<\/jats:p>\n          <jats:p\/>\n          <jats:p>\n            We propose\n            <jats:italic>LoRe<\/jats:italic>\n            , a programming model and compiler that automatically verifies developer-supplied safety properties for local-first applications.\n            <jats:italic>LoRe<\/jats:italic>\n            combines the declarative data flow of reactive programming with static analysis and verification techniques to precisely determine concurrent interactions that violate safety invariants and to selectively employ strong consistency through coordination where required. We propose a formalized proof principle and demonstrate how to automate the process in a prototype implementation that outputs verified executable code. Our evaluation shows that\n            <jats:italic>LoRe<\/jats:italic>\n            simplifies the development of safe local-first software when compared to state-of-the-art approaches and that verification times are acceptable.\n          <\/jats:p>","DOI":"10.1145\/3633769","type":"journal-article","created":{"date-parts":[[2023,12,1]],"date-time":"2023-12-01T11:45:47Z","timestamp":1701431147000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["LoRe: A Programming Model for Verifiably Safe Local-first Software"],"prefix":"10.1145","volume":"46","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9959-5099","authenticated-orcid":false,"given":"Julian","family":"Haas","sequence":"first","affiliation":[{"name":"Technische Universit\u00e4t Darmstadt, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4583-1791","authenticated-orcid":false,"given":"Ragnar","family":"Mogk","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t Darmstadt, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2900-7252","authenticated-orcid":false,"given":"Elena","family":"Yanakieva","sequence":"additional","affiliation":[{"name":"Rheinland-Pf\u00e4lzische Technische Universit\u00e4t Kaiserslautern-Landau, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1654-6118","authenticated-orcid":false,"given":"Annette","family":"Bieniusa","sequence":"additional","affiliation":[{"name":"Rheinland-Pf\u00e4lzische Technische Universit\u00e4t Kaiserslautern-Landau, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6563-7537","authenticated-orcid":false,"given":"Mira","family":"Mezini","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t Darmstadt, Germany, and National Research Center for Applied Cybersecurity (ATHENE), Germany, and Hessian Center for Artificial Intelligence (hessian.AI), Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,15]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICDCS.2016.98"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICDE.2014.6816639"},{"key":"e_1_3_2_4_2","volume-title":"Proceedings of the Conference on Innovative Data Systems Research (CIDR\u201911)","author":"Alvaro Peter","year":"2011","unstructured":"Peter Alvaro, Neil Conway, Joseph M. Hellerstein, and William R. Marczak. 2011. Consistency analysis in Bloom: A calm and collected approach. In Proceedings of the Conference on Innovative Data Systems Research (CIDR\u201911). Citeseer. Retrieved from http:\/\/cidrdb.org\/cidr2011\/Papers\/CIDR11_Paper35.pdf"},{"key":"e_1_3_2_5_2","unstructured":"Automerge contributors. 2023. Automerge: Build Local-First Software. Retrieved from https:\/\/automerge.org\/. Accessed on 2023-04-19."},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.14778\/2735508.2735509"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.14778\/3297753.3297760"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/2741948.2741972"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2723872.2723889"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2012.37"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2023.9"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485484"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-22496-7_3"},{"key":"e_1_3_2_15_2","volume-title":"An Empirical Study on Reactive Programming","author":"Dinser Moritz","year":"2021","unstructured":"Moritz Dinser. 2021. An Empirical Study on Reactive Programming. Master\u2019s thesis. Technische Universit\u00e4t Darmstadt. Retrieved from http:\/\/tubama.ulb.tu-darmstadt.de\/id\/eprint\/30079"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3276477"},{"key":"e_1_3_2_17_2","unstructured":"Seph Gentle. 2021. 5000x faster CRDTs: An Adventure in Optimization. Retrieved from https:\/\/josephg.com\/blog\/crdts-go-brrr\/"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133933"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837625"},{"key":"e_1_3_2_20_2","unstructured":"Joseph M. Hellerstein and Peter Alvaro. 2019. Keeping CALM: When distributed consistency is easy. Retrieved from http:\/\/arxiv.org\/abs\/1901.01930"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290387"},{"key":"e_1_3_2_22_2","unstructured":"Meta Platforms Inc. 2023. React: The Library for Web and Native User Interfaces. Retrieved from https:\/\/reactjs.org\/"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3276534"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3360580"},{"key":"e_1_3_2_25_2","volume-title":"Designing Data-Intensive Applications: The Big Ideas Behind Reliable, Scalable, and Maintainable Systems","author":"Kleppmann Martin","year":"2017","unstructured":"Martin Kleppmann. 2017. Designing Data-Intensive Applications: The Big Ideas Behind Reliable, Scalable, and Maintainable Systems. O\u2019Reilly. Retrieved from https:\/\/dataintensive.net\/"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3359591.3359737"},{"key":"e_1_3_2_27_2","volume-title":"ACM SIGPLAN Commercial Users of Functional Programming","author":"Klophaus Rusty","year":"2010","unstructured":"Rusty Klophaus. 2010. Riak core: Building distributed applications without shared state. In ACM SIGPLAN Commercial Users of Functional Programming. ACM, New York, NY."},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428256"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27919-5"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563336"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3341710"},{"key":"e_1_3_2_33_2","volume-title":"Proceedings of the USENIX Annual Technical Conference (USENIX ATC\u201914)","author":"Li Cheng","year":"2014","unstructured":"Cheng Li, Jo\u00e3o Leit\u00e3o, Allen Clement, Nuno M. Pregui\u00e7a, Rodrigo Rodrigues, and Viktor Vafeiadis. 2014. Automating the choice of consistency levels in replicated systems. In Proceedings of the USENIX Annual Technical Conference (USENIX ATC\u201914). USENIX Association, Philadelphia, PA. Retrieved from https:\/\/www.usenix.org\/conference\/atc14\/technical-sessions\/presentation\/li_cheng_2"},{"key":"e_1_3_2_34_2","first-page":"265","article-title":"Making geo-replicated systems fast as possible, consistent when necessary","author":"Li Cheng","year":"2012","unstructured":"Cheng Li, Daniel Porto, Allen Clement, Johannes Gehrke, Nuno Preguic, and Rodrigo Rodrigues. 2012. Making geo-replicated systems fast as possible, consistent when necessary. In Proceedings of the 10th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201912). 265\u2013278. Retrieved from https:\/\/www.usenix.org\/conference\/osdi12\/technical-sessions\/presentation\/li","journal-title":"Proceedings of the 10th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201912)"},{"key":"e_1_3_2_35_2","volume-title":"University of Texas at Austin Tech Report","author":"Mahajan Prince","year":"2011","unstructured":"Prince Mahajan, Lorenzo Alvisi, Mike Dahlin, et\u00a0al. 2011. Consistency, availability, and convergence. University of Texas at Austin Tech Report. Retrieved from https:\/\/www.cs.utexas.edu\/users\/dahlin\/papers\/cac-tr.pdf"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/2790449.2790525"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192375"},{"key":"e_1_3_2_38_2","volume-title":"Proceedings of the 32nd European Conference on Object-Oriented Programming (ECOOP\u201918)","volume":"109","author":"Mogk Ragnar","year":"2018","unstructured":"Ragnar Mogk, Lars Baumg\u00e4rtner, Guido Salvaneschi, Bernd Freisleben, and Mira Mezini. 2018. Fault-tolerant distributed reactive programming. In Proceedings of the 32nd European Conference on Object-Oriented Programming (ECOOP\u201918), Vol. 109. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany."},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3360570"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3276954.3276957"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_20"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/2957276.2957310"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-02654-1_13"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.1806.10254"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2017.2655524"},{"key":"e_1_3_2_47_2","unstructured":"Marc Shapiro Annette Bieniusa Nuno M. Pregui\u00e7a Valter Balegas and Christopher Meiklejohn. 2018. Just-right consistency: Reconciling availability and safety. Retrieved from http:\/\/arxiv.org\/abs\/1801.06340"},{"key":"e_1_3_2_48_2","first-page":"50","volume-title":"A Comprehensive Study of Convergent and Commutative Replicated Data Types","author":"Shapiro Marc","year":"2011","unstructured":"Marc Shapiro, Nuno Pregui\u00e7a, Carlos Baquero, and Marek Zawirski. 2011. A Comprehensive Study of Convergent and Commutative Replicated Data Types. Research Report RR-7506. Inria\u2013Centre Paris-Rocquencourt; INRIA. 50 pages. Retrieved from https:\/\/hal.inria.fr\/inria-00555588"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737981"},{"key":"e_1_3_2_50_2","unstructured":"TPC. 2021. TPC-C Specification 5.11.0. Retrieved from http:\/\/tpc.org\/TPC_Documents_Current_Versions\/pdf\/tpc-c_v5.11.0.pdf"},{"key":"e_1_3_2_51_2","article-title":"Viperproject\/Silicon Github Repository","year":"2021","unstructured":"Viper. 2021. Viperproject\/Silicon Github Repository. Viper Project. Retrieved from https:\/\/github.com\/viperproject\/silicon","journal-title":"Viper Project"},{"key":"e_1_3_2_52_2","unstructured":"Matthew Weidner Heather Miller Huairui Qi Maxime Kjaer Ria Pradeep Benito Geordie and Christopher Meiklejohn. 2022. Collabs: Composable Collaborative Data Structures. Retrieved from 2212.02618"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.14778\/3275536.3275538"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591276"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3633769","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3633769","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:35:48Z","timestamp":1750178148000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3633769"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,15]]},"references-count":53,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,3,31]]}},"alternative-id":["10.1145\/3633769"],"URL":"https:\/\/doi.org\/10.1145\/3633769","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,15]]},"assertion":[{"value":"2023-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-11-03","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-01-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}