{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:21:32Z","timestamp":1760059292388,"version":"build-2065373602"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>Refinement relates an abstract system model to a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development of substantial verified systems. Nevertheless, existing refinement techniques have limitations that impede their practical usefulness. Top-down refinement techniques that automatically generate executable code generally produce implementations with sub-optimal performance. Bottom-up refinement allows one to reason about existing, efficient implementations, but imposes strict requirements on the structure of the code, the structure of the refinement proofs, as well as the employed verification logic and tools.<\/jats:p>\n          <jats:p>\n            In this paper, we present a novel bottom-up refinement methodology that removes these limitations. Our methodology uses the familiar notion of guarded transition systems to express abstract models, but combines guards with a novel notion of\n            <jats:italic toggle=\"yes\">locally inductive invariants<\/jats:italic>\n            to relate the abstract model\n            <jats:italic toggle=\"yes\">locally<\/jats:italic>\n            to concrete state. This approach is much more flexible than standard coupling invariants; in particular, it supports a wide range of program structures, data representations, and proof structures. We integrate our methodology as a library into Rust, leveraging the Rust type system to reason about ownership of guards. This integration allows one to use our methodology with an off-the-shelf Rust verification tool. It also facilitates practical applications, as we demonstrate on a number of substantial case studies including a concurrent implementation of Memcached.\n          <\/jats:p>","DOI":"10.1145\/3763119","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"1921-1948","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A Refinement Methodology for Distributed Programs in Rust"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9284-9161","authenticated-orcid":false,"given":"Aurel","family":"B\u00edl\u00fd","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4671-4132","authenticated-orcid":false,"given":"Jo\u00e3o","family":"Pereira","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7001-2566","authenticated-orcid":false,"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158153"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2016.0331"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","unstructured":"Aurel B\u00edl\u00fd Jo\u00e3o Pereira and Peter M\u00fcller. 2025. A Refinement Methodology for Distributed Programs in Rust (artefact). https:\/\/doi.org\/10.5281\/zenodo.15753818 10.5281\/zenodo.15753818","DOI":"10.5281\/zenodo.15753818"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_2_2_7_1","unstructured":"Coq Contributors. 1989. Coq Proof Assistant. https:\/\/coq.inria.fr\/"},{"key":"e_1_2_2_8_1","unstructured":"Isabelle Contributors. 1986. Isabelle Proof Assistant. https:\/\/isabelle.in.tum.de\/"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_16"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_2_2_12_1","unstructured":"Marie Farrell Peter Lammich Marieke Huismann Rosemary Monahan Peter M\u00fcller and Mattias Ullbrich. 2022. VerifyThis 2022 Program Verification Competition. https:\/\/www.pm.inf.ethz.ch\/research\/verifythis\/Archive\/2022.html"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1012889.1012894"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_2_2_15_1","volume-title":"Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems. In 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23)","author":"Hance Travis","year":"2023","unstructured":"Travis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell, and Bryan Parno. 2023. Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems. In 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23). USENIX Association, Boston, MA. 911\u2013929. isbn:978-1-939133-34-2 https:\/\/www.usenix.org\/conference\/osdi23\/presentation\/hance"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3068608"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_26"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_21_1","volume-title":"International Standard ISO\/IEC 14882:2020(E) - Programming Language C++","author":"ISO.","unstructured":"ISO. 2021. International Standard ISO\/IEC 14882:2020(E) - Programming Language C++. International Organization for Standardization (ISO), Geneva, Switzerland."},{"key":"e_1_2_2_22_1","volume-title":"Summers","author":"Juhasz Uri","year":"2014","unstructured":"Uri Juhasz, Ioannis T. Kassios, Peter M\u00fcller, Milo\u0161 Nov\u00e1\u010dek, Malte Schwerhoff, and Alexander J. Summers. 2014. Viper: A Verification Infrastructure for Permission-Based Reasoning. 21 p. pages. http:\/\/hdl.handle.net\/20.500.11850\/85086"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676980"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294106"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_14"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_13"},{"key":"e_1_2_2_27_1","volume-title":"A Verified and Scalable Hash Table for the TLC Model Checker. Master\u2019s thesis","author":"Kuppe Markus A","unstructured":"Markus A Kuppe. 2017. A Verified and Scalable Hash Table for the TLC Model Checker. Master\u2019s thesis. University of Hamburg."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_2_2_29_1","volume-title":"The Part-Time Parliament","author":"Lamport Leslie","unstructured":"Leslie Lamport. 1998. The Part-Time Parliament. Association for Computing Machinery. isbn:978-1-4503-7270-1 https:\/\/dl.acm.org\/citation.cfm?id=3335939"},{"key":"e_1_2_2_30_1","unstructured":"Leslie Lamport. 2019. The Paxos Algorithm or How to Win a Turing Award. https:\/\/lamport.azurewebsites.net\/tla\/paxos-algorithm.html"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3694715.3695952"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_9"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","unstructured":"K. R. M. Leino and V. W\u00fcstholz. 2014. The Dafny Integrated Development Environment. In 1st Workshop on Formal Integrated Development Environment Catherine Dubois Dimitra Giannakopoulou and Dominique M\u00e9ry (Eds.) (Electronic Proceedings in Theoretical Computer Science Vol. 149). Open Publishing Association 3\u201315. https:\/\/doi.org\/10.4204\/EPTCS.149.2 10.4204\/EPTCS.149.2","DOI":"10.4204\/EPTCS.149.2"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837622"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","unstructured":"Richard J. Lipton. 1975. Reduction: a new method of proving properties of systems of processes. 78\u201386. isbn:9781450373517 https:\/\/doi.org\/10.1145\/512976.512985 10.1145\/512976.512985","DOI":"10.1145\/512976.512985"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-55754-6_2"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385971"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692956.2663188"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-34968-4_22"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_7"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_22"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_2_43_1","unstructured":"Jan Sch\u00e4r. 2023. Proving Refinement in a Rust Verifier. Master\u2019s thesis. ETH Zurich."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3600006.3613172"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428220"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034811"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632851"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763119","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:46:52Z","timestamp":1760032012000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763119"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":52,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763119"],"URL":"https:\/\/doi.org\/10.1145\/3763119","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}