[{"file":[{"content_type":"application/pdf","date_updated":"2026-02-12T13:51:03Z","success":1,"file_id":"21221","date_created":"2026-02-12T13:51:03Z","access_level":"open_access","checksum":"79be391061efbf9542638996959ce11a","relation":"main_file","file_name":"2026_ProcACMProgrammingLanguages_Mueck.pdf","file_size":1058876,"creator":"dernst"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png"},"date_published":"2026-01-08T00:00:00Z","department":[{"_id":"MiSa"}],"abstract":[{"text":"It is common for programmers to assemble their programs from a combination of trusted and untrusted components. In this context, a trusted program component is said to be robustly safe if it behaves safely when linked against arbitrary untrusted code. Prior work has shown how various encapsulation mechanisms (in both high- and low-level languages) can be used to protect code so that it is robustly safe, but none of the existing work has explored how robust safety can be achieved in a patently unsafe language like C.\r\nIn this paper, we show how to bring robust safety to a simple yet representative C-like language we call Rec. Although Rec (like C) is inherently ”dangerous” and thus not robustly safe, we can ”save” Rec programs via compilation to Cap, a CHERI-like capability machine. To formalize the benefits of such a hardening compiler, we develop Reckon, a separation logic for verifying robust safety of Rec programs. Reckon is not sound under Rec’s unsafe, C-like semantics, but it is sound when Rec programs are hardened via compilation and linked against untrusted code running on Cap. As a crucial step in proving soundness of Reckon, we introduce a novel technique of semantic back-translation, which we formalize by building on the DimSum framework for multi-language semantics. All our results are mechanized in the Rocq prover.","lang":"eng"}],"fulldoi":"https://doi.org/10.1145/3776682","language":[{"iso":"eng"}],"oa_version":"Published Version","PlanS_conform":"1","publication_identifier":{"eissn":["2475-1421"]},"publication_status":"published","scopus_import":"1","OA_place":"publisher","author":[{"first_name":"Niklas","last_name":"Mück","full_name":"Mück, Niklas"},{"first_name":"Aïna Linn","full_name":"Georges, Aïna Linn","last_name":"Georges"},{"full_name":"Dreyer, Derek","last_name":"Dreyer","first_name":"Derek"},{"first_name":"Deepak","last_name":"Garg","full_name":"Garg, Deepak"},{"full_name":"Sammler, Michael Joachim","last_name":"Sammler","id":"510d3901-2a03-11ee-914d-d9ae9011f0a7","first_name":"Michael Joachim"}],"has_accepted_license":"1","date_updated":"2026-02-12T13:53:04Z","publisher":"Association for Computing Machinery","year":"2026","volume":10,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Endangered by the language but saved by the compiler: Robust safety via semantic back-translation","file_date_updated":"2026-02-12T13:51:03Z","date_created":"2026-01-25T23:01:40Z","publication":"Proceedings of the ACM on Programming Languages","_id":"21041","article_type":"original","quality_controlled":"1","day":"08","oa":1,"month":"01","citation":{"chicago":"Mück, Niklas, Aïna Linn Georges, Derek Dreyer, Deepak Garg, and Michael Joachim Sammler. “Endangered by the Language but Saved by the Compiler: Robust Safety via Semantic Back-Translation.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2026. <a href=\"https://doi.org/10.1145/3776682\">https://doi.org/10.1145/3776682</a>.","short":"N. Mück, A.L. Georges, D. Dreyer, D. Garg, M.J. Sammler, Proceedings of the ACM on Programming Languages 10 (2026) 1153–1182.","ista":"Mück N, Georges AL, Dreyer D, Garg D, Sammler MJ. 2026. Endangered by the language but saved by the compiler: Robust safety via semantic back-translation. Proceedings of the ACM on Programming Languages. 10, 1153–1182.","ama":"Mück N, Georges AL, Dreyer D, Garg D, Sammler MJ. Endangered by the language but saved by the compiler: Robust safety via semantic back-translation. <i>Proceedings of the ACM on Programming Languages</i>. 2026;10:1153-1182. doi:<a href=\"https://doi.org/10.1145/3776682\">10.1145/3776682</a>","mla":"Mück, Niklas, et al. “Endangered by the Language but Saved by the Compiler: Robust Safety via Semantic Back-Translation.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 10, Association for Computing Machinery, 2026, pp. 1153–82, doi:<a href=\"https://doi.org/10.1145/3776682\">10.1145/3776682</a>.","ieee":"N. Mück, A. L. Georges, D. Dreyer, D. Garg, and M. J. Sammler, “Endangered by the language but saved by the compiler: Robust safety via semantic back-translation,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 10. Association for Computing Machinery, pp. 1153–1182, 2026.","apa":"Mück, N., Georges, A. L., Dreyer, D., Garg, D., &#38; Sammler, M. J. (2026). Endangered by the language but saved by the compiler: Robust safety via semantic back-translation. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3776682\">https://doi.org/10.1145/3776682</a>"},"status":"public","OA_type":"hybrid","type":"journal_article","page":"1153-1182","doi":"10.1145/3776682","intvolume":"        10","ddc":["000"],"article_processing_charge":"Yes (via OA deal)"},{"title":"A recipe for modular verification of generic tree traversals","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"start_date":"2026-01-12","name":"CPP: Conference on Certified Programs and Proofs","end_date":"2026-01-13","location":"Rennes, France"},"day":"08","quality_controlled":"1","oa":1,"file_date_updated":"2026-02-16T08:40:29Z","date_created":"2026-02-01T23:01:43Z","publication":"Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs","_id":"21133","type":"conference","status":"public","OA_type":"gold","month":"01","citation":{"ama":"Elbeheiry L, Sammler MJ, Krebbers R, Dreyer D, Garg D. A recipe for modular verification of generic tree traversals. In: <i>Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs</i>. Association for Computing Machinery; 2026:339-352. doi:<a href=\"https://doi.org/10.1145/3779031.3779110\">10.1145/3779031.3779110</a>","ista":"Elbeheiry L, Sammler MJ, Krebbers R, Dreyer D, Garg D. 2026. A recipe for modular verification of generic tree traversals. Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP: Conference on Certified Programs and Proofs, 339–352.","chicago":"Elbeheiry, Laila, Michael Joachim Sammler, Robbert Krebbers, Derek Dreyer, and Deepak Garg. “A Recipe for Modular Verification of Generic Tree Traversals.” In <i>Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs</i>, 339–52. Association for Computing Machinery, 2026. <a href=\"https://doi.org/10.1145/3779031.3779110\">https://doi.org/10.1145/3779031.3779110</a>.","short":"L. Elbeheiry, M.J. Sammler, R. Krebbers, D. Dreyer, D. Garg, in:, Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, Association for Computing Machinery, 2026, pp. 339–352.","apa":"Elbeheiry, L., Sammler, M. J., Krebbers, R., Dreyer, D., &#38; Garg, D. (2026). A recipe for modular verification of generic tree traversals. In <i>Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs</i> (pp. 339–352). Rennes, France: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3779031.3779110\">https://doi.org/10.1145/3779031.3779110</a>","ieee":"L. Elbeheiry, M. J. Sammler, R. Krebbers, D. Dreyer, and D. Garg, “A recipe for modular verification of generic tree traversals,” in <i>Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs</i>, Rennes, France, 2026, pp. 339–352.","mla":"Elbeheiry, Laila, et al. “A Recipe for Modular Verification of Generic Tree Traversals.” <i>Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs</i>, Association for Computing Machinery, 2026, pp. 339–52, doi:<a href=\"https://doi.org/10.1145/3779031.3779110\">10.1145/3779031.3779110</a>."},"ddc":["000"],"article_processing_charge":"No","page":"339-352","doi":"10.1145/3779031.3779110","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png"},"file":[{"creator":"dernst","file_size":811872,"file_name":"2026_CPP_Elbeheiry.pdf","relation":"main_file","checksum":"7df99991493e907d83a197151f378e3e","access_level":"open_access","date_created":"2026-02-16T08:40:29Z","file_id":"21225","date_updated":"2026-02-16T08:40:29Z","success":1,"content_type":"application/pdf"}],"fulldoi":"https://doi.org/10.1145/3779031.3779110","acknowledgement":"We thank the anonymous reviewers for their insightful suggestions. This research is supported in part by generous awards from Android Security’s ASPIRE program and from Google Research. The third author is supported, in part, by ERC grant COCONUT (grant no. 101171349), funded by the European Union. Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council Executive Agency. Neither the European Union nor the granting authority can be held responsible for them.","language":[{"iso":"eng"}],"date_published":"2026-01-08T00:00:00Z","department":[{"_id":"MiSa"}],"abstract":[{"lang":"eng","text":"Data structures based on trees and tree traversals are ubiquitous in computer systems. Many low-level programs, including some implementations of critical systems like page tables and the web browser DOM, rely on generic tree-traversal functions that traverse tree nodes in a pre-determined order, applying a client-provided operation to each visited node. Developing a general approach to specifying and verifying such traversals is tricky since the client-provided per-node operation can be stateful and may potentially depend on or modify the structure of the tree being traversed.\r\nIn this paper, we present a recipe for (semi-)automated verification of such generic, stateful tree traversals. Our recipe is (a) general: it applies to a range of tree traversals, in particular, pre-, post- and in-order depth-first traversals; (b) modular: parts of a traversal’s proof can be reused in verifying other similar traversals; (c) expressive: using the specification of a tree traversal, we can verify clients that use the traversal in a variety of different ways; and (d) automatable: many proof obligations can be discharged automatically.\r\nAt the heart of our recipe is a novel use of tree zippers to represent a logical abstraction of the tree traversal state, and zipper transitions as an abstraction of traversal steps. We realize our recipe in the RefinedC framework in Rocq, which allows us to verify a number of different tree traversals and their clients written in C."}],"publication_identifier":{"isbn":["9798400723414"]},"oa_version":"Published Version","date_updated":"2026-02-16T08:43:24Z","has_accepted_license":"1","publisher":"Association for Computing Machinery","year":"2026","publication_status":"published","scopus_import":"1","OA_place":"publisher","author":[{"full_name":"Elbeheiry, Laila","last_name":"Elbeheiry","first_name":"Laila"},{"last_name":"Sammler","full_name":"Sammler, Michael Joachim","id":"510d3901-2a03-11ee-914d-d9ae9011f0a7","first_name":"Michael Joachim"},{"first_name":"Robbert","last_name":"Krebbers","full_name":"Krebbers, Robbert"},{"first_name":"Derek","last_name":"Dreyer","full_name":"Dreyer, Derek"},{"full_name":"Garg, Deepak","last_name":"Garg","first_name":"Deepak"}]},{"intvolume":"         9","doi":"10.1145/3704847","page":"300-331","article_processing_charge":"No","OA_type":"hybrid","status":"public","month":"01","citation":{"apa":"Vistrup, M., Sammler, M. J., &#38; Jung, R. (2025). Program logics à la Carte. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3704847\">https://doi.org/10.1145/3704847</a>","ieee":"M. Vistrup, M. J. Sammler, and R. Jung, “Program logics à la Carte,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 9, no. POPL. Association for Computing Machinery, pp. 300–331, 2025.","mla":"Vistrup, Max, et al. “Program Logics à La Carte.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 9, no. POPL, Association for Computing Machinery, 2025, pp. 300–31, doi:<a href=\"https://doi.org/10.1145/3704847\">10.1145/3704847</a>.","ama":"Vistrup M, Sammler MJ, Jung R. Program logics à la Carte. <i>Proceedings of the ACM on Programming Languages</i>. 2025;9(POPL):300-331. doi:<a href=\"https://doi.org/10.1145/3704847\">10.1145/3704847</a>","ista":"Vistrup M, Sammler MJ, Jung R. 2025. Program logics à la Carte. Proceedings of the ACM on Programming Languages. 9(POPL), 300–331.","chicago":"Vistrup, Max, Michael Joachim Sammler, and Ralf Jung. “Program Logics à La Carte.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2025. <a href=\"https://doi.org/10.1145/3704847\">https://doi.org/10.1145/3704847</a>.","short":"M. Vistrup, M.J. Sammler, R. Jung, Proceedings of the ACM on Programming Languages 9 (2025) 300–331."},"issue":"POPL","type":"journal_article","publication":"Proceedings of the ACM on Programming Languages","_id":"21052","date_created":"2026-01-28T06:35:47Z","oa":1,"quality_controlled":"1","day":"09","article_type":"original","main_file_link":[{"open_access":"1"}],"title":"Program logics à la Carte","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Vistrup","full_name":"Vistrup, Max","first_name":"Max"},{"first_name":"Michael Joachim","id":"510d3901-2a03-11ee-914d-d9ae9011f0a7","last_name":"Sammler","full_name":"Sammler, Michael Joachim"},{"full_name":"Jung, Ralf","last_name":"Jung","first_name":"Ralf"}],"scopus_import":"1","OA_place":"publisher","publication_status":"published","volume":9,"year":"2025","publisher":"Association for Computing Machinery","date_updated":"2026-02-09T06:19:36Z","has_accepted_license":"1","oa_version":"Published Version","publication_identifier":{"issn":["2475-1421"]},"PlanS_conform":"1","abstract":[{"text":"Program logics have proven a successful strategy for verification of complex programs. By providing local reasoning and means of abstraction and composition, they allow reasoning principles for individual components of a program to be combined to prove guarantees about a whole program. Crucially, these components and their proofs can be reused. However, this reuse is only available once the program logic has been defined. It is a frustrating fact of the status quo that whoever defines a new program logic must establish every part, both semantics and proof rules, from scratch. In spite of programming languages and program logics typically sharing many core features, reuse is generally not available across languages. Even inside one language, if the same underlying operation appears in multiple language primitives, reuse is typically not possible when establishing proof rules for the program logic.\r\nTo enable reuse across and inside languages when defining complex program logics (and proving them sound), we serve program logics à la carte by combining program logic fragments for the various effects of the language. Among other language features, the menu includes shared state, concurrency, and non-determinism as reusable, composable blocks that can be combined to define a program logic modularly. Our theory builds on ITrees as a framework to express language semantics and Iris as the underlying separation logic; the work has been mechanized in the Coq proof assistant.","lang":"eng"}],"date_published":"2025-01-09T00:00:00Z","extern":"1","language":[{"iso":"eng"}],"fulldoi":"https://doi.org/10.1145/3704847","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png"}},{"abstract":[{"lang":"eng","text":"Program verification tools are often implemented as front-end translations of an input program into an intermediate verification language (IVL) such as Boogie, GIL, Viper, or Why3. The resulting IVL program is then verified using an existing back-end verifier. A soundness proof for such a translational verifier needs to relate the input program and verification logic to the semantics of the IVL, which in turn needs to be connected with the verification logic implemented in the back-end verifiers. Performing such proofs is challenging due to the large semantic gap between the input and output programs and logics, especially for complex verification logics such as separation logic.\r\nThis paper presents a formal framework for reasoning about translational separation logic verifiers. At its center is a generic core IVL that captures the essence of different separation logics. We define its operational semantics and formally connect it to two different back-end verifiers, which use symbolic execution and verification condition generation, resp. Crucially, this semantics uses angelic non-determinism to enable the application of different proof search algorithms and heuristics in the back-end verifiers. An axiomatic semantics for the core IVL simplifies reasoning about the front-end translation by performing essential proof steps once and for all in the equivalence proof with the operational semantics rather than for each concrete front-end translation.\r\nWe illustrate the usefulness of our formal framework by instantiating our core IVL with elements of Viper and connecting it to two Viper back-ends as well as a front-end for concurrent separation logic. All our technical results have been formalized in Isabelle/HOL, including the core IVL and its semantics, the semantics of two back-ends for a subset of Viper, and all proofs."}],"extern":"1","date_published":"2025-01-09T00:00:00Z","language":[{"iso":"eng"}],"arxiv":1,"fulldoi":"https://doi.org/10.1145/3704856","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png"},"external_id":{"arxiv":["2407.20002"]},"OA_place":"publisher","author":[{"last_name":"Dardinier","full_name":"Dardinier, Thibault","first_name":"Thibault"},{"full_name":"Sammler, Michael Joachim","last_name":"Sammler","id":"510d3901-2a03-11ee-914d-d9ae9011f0a7","first_name":"Michael Joachim"},{"first_name":"Gaurav","last_name":"Parthasarathy","full_name":"Parthasarathy, Gaurav"},{"full_name":"Summers, Alexander J.","last_name":"Summers","first_name":"Alexander J."},{"first_name":"Peter","full_name":"Müller, Peter","last_name":"Müller"}],"publication_status":"published","year":"2025","volume":9,"has_accepted_license":"1","date_updated":"2026-02-09T06:25:01Z","publisher":"Association for Computing Machinery","oa_version":"Published Version","publication_identifier":{"issn":["2475-1421"]},"PlanS_conform":"1","date_created":"2026-01-28T06:36:57Z","_id":"21053","publication":"Proceedings of the ACM on Programming Languages","article_type":"original","quality_controlled":"1","day":"09","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Formal foundations for translational separation logic verifiers","page":"569-599","doi":"10.1145/3704856","intvolume":"         9","article_processing_charge":"No","ddc":["000"],"status":"public","citation":{"apa":"Dardinier, T., Sammler, M. J., Parthasarathy, G., Summers, A. J., &#38; Müller, P. (2025). Formal foundations for translational separation logic verifiers. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3704856\">https://doi.org/10.1145/3704856</a>","mla":"Dardinier, Thibault, et al. “Formal Foundations for Translational Separation Logic Verifiers.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 9, no. POPL, Association for Computing Machinery, 2025, pp. 569–99, doi:<a href=\"https://doi.org/10.1145/3704856\">10.1145/3704856</a>.","ieee":"T. Dardinier, M. J. Sammler, G. Parthasarathy, A. J. Summers, and P. Müller, “Formal foundations for translational separation logic verifiers,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 9, no. POPL. Association for Computing Machinery, pp. 569–599, 2025.","ista":"Dardinier T, Sammler MJ, Parthasarathy G, Summers AJ, Müller P. 2025. Formal foundations for translational separation logic verifiers. Proceedings of the ACM on Programming Languages. 9(POPL), 569–599.","ama":"Dardinier T, Sammler MJ, Parthasarathy G, Summers AJ, Müller P. Formal foundations for translational separation logic verifiers. <i>Proceedings of the ACM on Programming Languages</i>. 2025;9(POPL):569-599. doi:<a href=\"https://doi.org/10.1145/3704856\">10.1145/3704856</a>","short":"T. Dardinier, M.J. Sammler, G. Parthasarathy, A.J. Summers, P. Müller, Proceedings of the ACM on Programming Languages 9 (2025) 569–599.","chicago":"Dardinier, Thibault, Michael Joachim Sammler, Gaurav Parthasarathy, Alexander J. Summers, and Peter Müller. “Formal Foundations for Translational Separation Logic Verifiers.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2025. <a href=\"https://doi.org/10.1145/3704856\">https://doi.org/10.1145/3704856</a>."},"OA_type":"hybrid","month":"01","type":"journal_article","issue":"POPL"},{"oa_version":"Published Version","corr_author":"1","publication_identifier":{"eissn":["2475-1421"]},"publication_status":"published","OA_place":"publisher","scopus_import":"1","author":[{"first_name":"Simon","last_name":"Spies","full_name":"Spies, Simon"},{"last_name":"Mück","full_name":"Mück, Niklas","first_name":"Niklas"},{"full_name":"Zeng, Haoyi","last_name":"Zeng","first_name":"Haoyi"},{"full_name":"Sammler, Michael Joachim","last_name":"Sammler","first_name":"Michael Joachim","id":"510d3901-2a03-11ee-914d-d9ae9011f0a7"},{"first_name":"Andrea","full_name":"Lattuada, Andrea","last_name":"Lattuada"},{"first_name":"Peter","last_name":"Müller","full_name":"Müller, Peter"},{"first_name":"Derek","last_name":"Dreyer","full_name":"Dreyer, Derek"}],"date_updated":"2025-06-30T09:10:11Z","has_accepted_license":"1","publisher":"Association for Computing Machinery","year":"2025","volume":9,"file":[{"file_size":843343,"creator":"dernst","file_id":"19938","success":1,"date_updated":"2025-06-30T09:01:08Z","content_type":"application/pdf","file_name":"2025_ProcACMProg_Spies.pdf","checksum":"6b72d84c10a10ba7cd1646e2c36dc1ff","date_created":"2025-06-30T09:01:08Z","access_level":"open_access","relation":"main_file"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png"},"date_published":"2025-06-01T00:00:00Z","department":[{"_id":"MiSa"}],"abstract":[{"text":"The separation logic framework Iris has been built on the premise that all assertions are stable, meaning they unconditionally enjoy the famous frame rule. This gives Iris—and the numerous program logics that build on it—very modular reasoning principles. But stability also comes at a cost. It excludes a core feature of the Viper verifier family, heap-dependent expression assertions, which lift program expressions to the assertion level in order to reduce redundancy between code and specifications and better facilitate SMT-based automation.\r\nIn this paper, we bring heap-dependent expression assertions to Iris with Daenerys. To do so, we must first revisit the very core of Iris, extending it with a new form of unstable resources (and adapting the frame rule accordingly). On top, we then build a program logic with heap-dependent expression assertions and lay the foundations for connecting Iris to SMT solvers. We apply Daenerys to several case studies, including some that go beyond what Viper and Iris can do individually and others that benefit from the connection to SMT.","lang":"eng"}],"fulldoi":"https://doi.org/10.1145/3729284","acknowledgement":"We would like to thank the anonymous reviewers for their helpful feedback and Alex Summers\r\nfor insightful discussions. This work was funded in part by a Google PhD Fellowship for the first\r\nauthor.","language":[{"iso":"eng"}],"OA_type":"hybrid","citation":{"chicago":"Spies, Simon, Niklas Mück, Haoyi Zeng, Michael Joachim Sammler, Andrea Lattuada, Peter Müller, and Derek Dreyer. “Destabilizing Iris.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2025. <a href=\"https://doi.org/10.1145/3729284\">https://doi.org/10.1145/3729284</a>.","short":"S. Spies, N. Mück, H. Zeng, M.J. Sammler, A. Lattuada, P. Müller, D. Dreyer, Proceedings of the ACM on Programming Languages 9 (2025) 848–873.","ama":"Spies S, Mück N, Zeng H, et al. Destabilizing Iris. <i>Proceedings of the ACM on Programming Languages</i>. 2025;9(PLDI):848-873. doi:<a href=\"https://doi.org/10.1145/3729284\">10.1145/3729284</a>","ista":"Spies S, Mück N, Zeng H, Sammler MJ, Lattuada A, Müller P, Dreyer D. 2025. Destabilizing Iris. Proceedings of the ACM on Programming Languages. 9(PLDI), 848–873.","mla":"Spies, Simon, et al. “Destabilizing Iris.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 9, no. PLDI, Association for Computing Machinery, 2025, pp. 848–73, doi:<a href=\"https://doi.org/10.1145/3729284\">10.1145/3729284</a>.","ieee":"S. Spies <i>et al.</i>, “Destabilizing Iris,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 9, no. PLDI. Association for Computing Machinery, pp. 848–873, 2025.","apa":"Spies, S., Mück, N., Zeng, H., Sammler, M. J., Lattuada, A., Müller, P., &#38; Dreyer, D. (2025). Destabilizing Iris. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3729284\">https://doi.org/10.1145/3729284</a>"},"month":"06","status":"public","type":"journal_article","issue":"PLDI","page":"848-873","intvolume":"         9","doi":"10.1145/3729284","ddc":["000"],"article_processing_charge":"Yes (in subscription journal)","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Destabilizing Iris","date_created":"2025-06-30T08:47:31Z","file_date_updated":"2025-06-30T09:01:08Z","publication":"Proceedings of the ACM on Programming Languages","_id":"19935","quality_controlled":"1","article_type":"original","day":"01","oa":1},{"language":[{"iso":"eng"}],"acknowledgement":"We would like to thank the anonymous reviewers for their helpful feedback.\r\nThis project has received funding from the European Research Council (ERC) under the European\r\nUnion’s Horizon 2020 research and innovation programme (grant agreement No 803111).","fulldoi":"https://doi.org/10.1145/3729249","abstract":[{"text":"There has been a recent upsurge of interest in formal, machine-checked verification of timing guarantees for C implementations of real-time system schedulers. However, prior work has only considered tick-based schedulers, which enjoy a clearly defined notion of time: the time \"quantum\". In this work, we present a new approach to real-time systems verification for interrupt-free schedulers, which are commonly used in deeply embedded and resource-constrained systems but which do not enjoy a natural notion of periodic time. Our approach builds on and connects two recently developed Rocq-based systems—RefinedC (for foundational C verification) and Prosa (for verified response-time analysis)—adapting the former to reason about timed traces and the latter to reason about overheads. We apply the resulting system, which we call RefinedProsa, to verify Rössl, a simple yet representative, fixed-priority, non-preemptive, interrupt-free scheduler implemented in C.","lang":"eng"}],"department":[{"_id":"MiSa"}],"date_published":"2025-06-13T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png"},"file":[{"access_level":"open_access","checksum":"8c18d777feb342a7265c54b16205ec4c","date_created":"2025-06-30T09:08:05Z","relation":"main_file","file_name":"2025_ProcACMProg_Bedarkar.pdf","content_type":"application/pdf","file_id":"19939","success":1,"date_updated":"2025-06-30T09:08:05Z","creator":"dernst","file_size":1043790}],"volume":9,"year":"2025","publisher":"Association for Computing Machinery","date_updated":"2025-06-30T09:09:55Z","has_accepted_license":"1","author":[{"first_name":"Kimaya","last_name":"Bedarkar","full_name":"Bedarkar, Kimaya"},{"first_name":"Laila","full_name":"Elbeheiry, Laila","last_name":"Elbeheiry"},{"last_name":"Sammler","full_name":"Sammler, Michael Joachim","id":"510d3901-2a03-11ee-914d-d9ae9011f0a7","first_name":"Michael Joachim"},{"first_name":"Lennard","last_name":"Gäher","full_name":"Gäher, Lennard"},{"first_name":"Björn","full_name":"Brandenburg, Björn","last_name":"Brandenburg"},{"last_name":"Dreyer","full_name":"Dreyer, Derek","first_name":"Derek"},{"full_name":"Garg, Deepak","last_name":"Garg","first_name":"Deepak"}],"OA_place":"publisher","scopus_import":"1","publication_status":"published","publication_identifier":{"issn":["2475-1421"]},"corr_author":"1","oa_version":"Published Version","oa":1,"article_type":"original","day":"13","quality_controlled":"1","publication":"Proceedings of the ACM on Programming Languages","_id":"19936","date_created":"2025-06-30T08:47:58Z","file_date_updated":"2025-06-30T09:08:05Z","title":"RefinedProsa: Connecting response-time analysis with C verification for interrupt-free schedulers","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"Yes (in subscription journal)","ddc":["000"],"intvolume":"         9","doi":"10.1145/3729249","page":"73-97","type":"journal_article","issue":"PLDI","citation":{"ama":"Bedarkar K, Elbeheiry L, Sammler MJ, et al. RefinedProsa: Connecting response-time analysis with C verification for interrupt-free schedulers. <i>Proceedings of the ACM on Programming Languages</i>. 2025;9(PLDI):73-97. doi:<a href=\"https://doi.org/10.1145/3729249\">10.1145/3729249</a>","ista":"Bedarkar K, Elbeheiry L, Sammler MJ, Gäher L, Brandenburg B, Dreyer D, Garg D. 2025. RefinedProsa: Connecting response-time analysis with C verification for interrupt-free schedulers. Proceedings of the ACM on Programming Languages. 9(PLDI), 73–97.","chicago":"Bedarkar, Kimaya, Laila Elbeheiry, Michael Joachim Sammler, Lennard Gäher, Björn Brandenburg, Derek Dreyer, and Deepak Garg. “RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2025. <a href=\"https://doi.org/10.1145/3729249\">https://doi.org/10.1145/3729249</a>.","short":"K. Bedarkar, L. Elbeheiry, M.J. Sammler, L. Gäher, B. Brandenburg, D. Dreyer, D. Garg, Proceedings of the ACM on Programming Languages 9 (2025) 73–97.","apa":"Bedarkar, K., Elbeheiry, L., Sammler, M. J., Gäher, L., Brandenburg, B., Dreyer, D., &#38; Garg, D. (2025). RefinedProsa: Connecting response-time analysis with C verification for interrupt-free schedulers. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3729249\">https://doi.org/10.1145/3729249</a>","mla":"Bedarkar, Kimaya, et al. “RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 9, no. PLDI, Association for Computing Machinery, 2025, pp. 73–97, doi:<a href=\"https://doi.org/10.1145/3729249\">10.1145/3729249</a>.","ieee":"K. Bedarkar <i>et al.</i>, “RefinedProsa: Connecting response-time analysis with C verification for interrupt-free schedulers,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 9, no. PLDI. Association for Computing Machinery, pp. 73–97, 2025."},"month":"06","OA_type":"hybrid","status":"public"},{"publication_status":"published","scopus_import":"1","author":[{"first_name":"Lennard","last_name":"Gäher","full_name":"Gäher, Lennard"},{"full_name":"Sammler, Michael Joachim","last_name":"Sammler","first_name":"Michael Joachim","id":"510d3901-2a03-11ee-914d-d9ae9011f0a7"},{"last_name":"Jung","full_name":"Jung, Ralf","first_name":"Ralf"},{"first_name":"Robbert","full_name":"Krebbers, Robbert","last_name":"Krebbers"},{"first_name":"Derek","full_name":"Dreyer, Derek","last_name":"Dreyer"}],"date_updated":"2024-09-10T07:16:49Z","publisher":"Association for Computing Machinery","year":"2024","volume":8,"oa_version":"Published Version","publication_identifier":{"issn":["2475-1421"]},"extern":"1","date_published":"2024-06-20T00:00:00Z","abstract":[{"lang":"eng","text":"Rust is a modern systems programming language whose ownership-based type system statically guarantees memory safety, making it particularly well-suited to the domain of safety-critical systems. In recent years, a wellspring of automated deductive verification tools have emerged for establishing functional correctness of Rust code. However, none of the previous tools produce foundational proofs (machine-checkable in a general-purpose proof assistant), and all of them are restricted to the safe fragment of Rust. This is a problem because the vast majority of Rust programs make use of unsafe code at critical points, such as in the implementation of widely-used APIs. We propose RefinedRust, a refinement type system—proven sound in the Coq proof assistant—with the goal of establishing foundational semi-automated functional correctness verification of both safe and unsafe Rust code. We have developed a prototype verification tool implementing RefinedRust. Our tool translates Rust code (with user annotations) into a model of Rust embedded in Coq, and then checks its adherence to the RefinedRust type system using separation logic automation in Coq. All proofs generated by RefinedRust are checked by the Coq proof assistant, so the automation and type system do not have to be trusted. We evaluate the effectiveness of RefinedRust by verifying a variant of Rust’s Vec implementation that involves intricate reasoning about unsafe pointer-manipulating code."}],"fulldoi":"https://doi.org/10.1145/3656422","language":[{"iso":"eng"}],"page":"1115-1139","intvolume":"         8","doi":"10.1145/3656422","article_processing_charge":"No","month":"06","status":"public","citation":{"ista":"Gäher L, Sammler MJ, Jung R, Krebbers R, Dreyer D. 2024. RefinedRust: A type system for high-assurance verification of rust programs. Proceedings of the ACM on Programming Languages. 8(PLDI), 1115–1139.","ama":"Gäher L, Sammler MJ, Jung R, Krebbers R, Dreyer D. RefinedRust: A type system for high-assurance verification of rust programs. <i>Proceedings of the ACM on Programming Languages</i>. 2024;8(PLDI):1115-1139. doi:<a href=\"https://doi.org/10.1145/3656422\">10.1145/3656422</a>","short":"L. Gäher, M.J. Sammler, R. Jung, R. Krebbers, D. Dreyer, Proceedings of the ACM on Programming Languages 8 (2024) 1115–1139.","chicago":"Gäher, Lennard, Michael Joachim Sammler, Ralf Jung, Robbert Krebbers, and Derek Dreyer. “RefinedRust: A Type System for High-Assurance Verification of Rust Programs.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2024. <a href=\"https://doi.org/10.1145/3656422\">https://doi.org/10.1145/3656422</a>.","apa":"Gäher, L., Sammler, M. J., Jung, R., Krebbers, R., &#38; Dreyer, D. (2024). RefinedRust: A type system for high-assurance verification of rust programs. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3656422\">https://doi.org/10.1145/3656422</a>","mla":"Gäher, Lennard, et al. “RefinedRust: A Type System for High-Assurance Verification of Rust Programs.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 8, no. PLDI, Association for Computing Machinery, 2024, pp. 1115–39, doi:<a href=\"https://doi.org/10.1145/3656422\">10.1145/3656422</a>.","ieee":"L. Gäher, M. J. Sammler, R. Jung, R. Krebbers, and D. Dreyer, “RefinedRust: A type system for high-assurance verification of rust programs,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 8, no. PLDI. Association for Computing Machinery, pp. 1115–1139, 2024."},"issue":"PLDI","type":"journal_article","date_created":"2024-09-05T07:52:27Z","_id":"17495","publication":"Proceedings of the ACM on Programming Languages","article_type":"original","day":"20","quality_controlled":"1","oa":1,"main_file_link":[{"url":"https://doi.org/10.1145/3656422","open_access":"1"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","title":"RefinedRust: A type system for high-assurance verification of rust programs"},{"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","title":"Quiver: Guided abductive inference of separation logic specifications in coq","main_file_link":[{"url":"https://doi.org/10.1145/3656413","open_access":"1"}],"publication":"Proceedings of the ACM on Programming Languages","_id":"17497","date_created":"2024-09-05T08:10:41Z","oa":1,"article_type":"original","day":"20","quality_controlled":"1","status":"public","month":"06","citation":{"chicago":"Spies, Simon, Lennard Gäher, Michael Joachim Sammler, and Derek Dreyer. “Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2024. <a href=\"https://doi.org/10.1145/3656413\">https://doi.org/10.1145/3656413</a>.","short":"S. Spies, L. Gäher, M.J. Sammler, D. Dreyer, Proceedings of the ACM on Programming Languages 8 (2024) 889–913.","ista":"Spies S, Gäher L, Sammler MJ, Dreyer D. 2024. Quiver: Guided abductive inference of separation logic specifications in coq. Proceedings of the ACM on Programming Languages. 8(PLDI), 889–913.","ama":"Spies S, Gäher L, Sammler MJ, Dreyer D. Quiver: Guided abductive inference of separation logic specifications in coq. <i>Proceedings of the ACM on Programming Languages</i>. 2024;8(PLDI):889-913. doi:<a href=\"https://doi.org/10.1145/3656413\">10.1145/3656413</a>","ieee":"S. Spies, L. Gäher, M. J. Sammler, and D. Dreyer, “Quiver: Guided abductive inference of separation logic specifications in coq,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 8, no. PLDI. Association for Computing Machinery, pp. 889–913, 2024.","mla":"Spies, Simon, et al. “Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 8, no. PLDI, Association for Computing Machinery, 2024, pp. 889–913, doi:<a href=\"https://doi.org/10.1145/3656413\">10.1145/3656413</a>.","apa":"Spies, S., Gäher, L., Sammler, M. J., &#38; Dreyer, D. (2024). Quiver: Guided abductive inference of separation logic specifications in coq. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3656413\">https://doi.org/10.1145/3656413</a>"},"type":"journal_article","issue":"PLDI","intvolume":"         8","doi":"10.1145/3656413","page":"889-913","article_processing_charge":"No","abstract":[{"lang":"eng","text":"Over the past two decades, there has been a great deal of progress on verification of full functional correctness of programs using separation logic, sometimes even producing “foundational” proofs in proof assistants like Coq. Unfortunately, even though existing approaches to this problem provide significant support for automated verification, they still incur a significant specification overhead: the user must supply the specification against which the program is verified, and the specification may be long, complex, or tedious to formulate. In this paper, we introduce Quiver, the first technique for inferring functional correctness specifications in separation logic while simultaneously verifying foundationally that they are correct. To guide Quiver towards the final specification, we take hints from the user in the form of a specification sketch, and then complete the sketch using inference. To do so, Quiver introduces a new abductive deductive verification technique, which integrates ideas from abductive inference (for specification inference) together with deductive separation logic automation (for foundational verification). The result is that users have to provide some guidance, but significantly less than with traditional deductive verification techniques based on separation logic. We have evaluated Quiver on a range of case studies, including code from popular open-source libraries."}],"date_published":"2024-06-20T00:00:00Z","extern":"1","language":[{"iso":"eng"}],"fulldoi":"https://doi.org/10.1145/3656413","oa_version":"Published Version","publication_identifier":{"issn":["2475-1421"]},"author":[{"first_name":"Simon","full_name":"Spies, Simon","last_name":"Spies"},{"first_name":"Lennard","last_name":"Gäher","full_name":"Gäher, Lennard"},{"last_name":"Sammler","full_name":"Sammler, Michael Joachim","id":"510d3901-2a03-11ee-914d-d9ae9011f0a7","first_name":"Michael Joachim"},{"first_name":"Derek","full_name":"Dreyer, Derek","last_name":"Dreyer"}],"scopus_import":"1","publication_status":"published","volume":8,"year":"2024","publisher":"Association for Computing Machinery","date_updated":"2024-09-10T12:00:57Z"},{"issue":"OOPSLA2","type":"journal_article","citation":{"apa":"Guéneau, A., Hostert, J., Spies, S., Sammler, M. J., Birkedal, L., &#38; Dreyer, D. (2023). Melocoton: A program logic for verified interoperability between OCaml and C. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3622823\">https://doi.org/10.1145/3622823</a>","ieee":"A. Guéneau, J. Hostert, S. Spies, M. J. Sammler, L. Birkedal, and D. Dreyer, “Melocoton: A program logic for verified interoperability between OCaml and C,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 7, no. OOPSLA2. Association for Computing Machinery, pp. 716–744, 2023.","mla":"Guéneau, Armaël, et al. “Melocoton: A Program Logic for Verified Interoperability between OCaml and C.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 7, no. OOPSLA2, Association for Computing Machinery, 2023, pp. 716–44, doi:<a href=\"https://doi.org/10.1145/3622823\">10.1145/3622823</a>.","ista":"Guéneau A, Hostert J, Spies S, Sammler MJ, Birkedal L, Dreyer D. 2023. Melocoton: A program logic for verified interoperability between OCaml and C. Proceedings of the ACM on Programming Languages. 7(OOPSLA2), 716–744.","ama":"Guéneau A, Hostert J, Spies S, Sammler MJ, Birkedal L, Dreyer D. Melocoton: A program logic for verified interoperability between OCaml and C. <i>Proceedings of the ACM on Programming Languages</i>. 2023;7(OOPSLA2):716-744. doi:<a href=\"https://doi.org/10.1145/3622823\">10.1145/3622823</a>","chicago":"Guéneau, Armaël, Johannes Hostert, Simon Spies, Michael Joachim Sammler, Lars Birkedal, and Derek Dreyer. “Melocoton: A Program Logic for Verified Interoperability between OCaml and C.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2023. <a href=\"https://doi.org/10.1145/3622823\">https://doi.org/10.1145/3622823</a>.","short":"A. Guéneau, J. Hostert, S. Spies, M.J. Sammler, L. Birkedal, D. Dreyer, Proceedings of the ACM on Programming Languages 7 (2023) 716–744."},"status":"public","month":"10","article_processing_charge":"No","page":"716-744","doi":"10.1145/3622823","intvolume":"         7","title":"Melocoton: A program logic for verified interoperability between OCaml and C","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1145/3622823"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","quality_controlled":"1","article_type":"original","day":"16","oa":1,"date_created":"2024-09-05T08:17:10Z","publication":"Proceedings of the ACM on Programming Languages","_id":"17498","publication_identifier":{"issn":["2475-1421"]},"oa_version":"Published Version","date_updated":"2024-09-10T09:04:24Z","publisher":"Association for Computing Machinery","year":"2023","volume":7,"publication_status":"published","scopus_import":"1","author":[{"first_name":"Armaël","last_name":"Guéneau","full_name":"Guéneau, Armaël"},{"first_name":"Johannes","last_name":"Hostert","full_name":"Hostert, Johannes"},{"full_name":"Spies, Simon","last_name":"Spies","first_name":"Simon"},{"last_name":"Sammler","full_name":"Sammler, Michael Joachim","id":"510d3901-2a03-11ee-914d-d9ae9011f0a7","first_name":"Michael Joachim"},{"first_name":"Lars","full_name":"Birkedal, Lars","last_name":"Birkedal"},{"first_name":"Derek","last_name":"Dreyer","full_name":"Dreyer, Derek"}],"fulldoi":"https://doi.org/10.1145/3622823","language":[{"iso":"eng"}],"extern":"1","date_published":"2023-10-16T00:00:00Z","abstract":[{"text":"In recent years, there has been tremendous progress on developing program logics for verifying the correctness of programs in a rich and diverse array of languages. Thus far, however, such logics have assumed that programs are written entirely in a single programming language. In practice, this assumption rarely holds since programs are often composed of components written in different programming languages, which interact with one another via some kind of foreign function interface (FFI). In this paper, we take the first steps towards the goal of developing program logics for multi-language verification. Specifically, we present Melocoton, a multi-language program verification system for reasoning about OCaml, C, and their interactions through the OCaml FFI. Melocoton consists of the first formal semantics of (a large subset of) the OCaml FFI—previously only described in prose in the OCaml manual—as well as the first program logic to reason about the interactions of program components written in OCaml and C. Melocoton is fully mechanized in Coq on top of the Iris separation logic framework.","lang":"eng"}]},{"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","main_file_link":[{"url":"https://doi.org/10.1145/3571232","open_access":"1"}],"title":"Conditional contextual refinement","quality_controlled":"1","article_type":"original","day":"11","oa":1,"date_created":"2024-09-05T08:21:51Z","publication":"Proceedings of the ACM on Programming Languages","_id":"17499","type":"journal_article","issue":"POPL","status":"public","citation":{"short":"Y. Song, M. Cho, D. Lee, C.-K. Hur, M.J. Sammler, D. Dreyer, Proceedings of the ACM on Programming Languages 7 (2023) 1121–1151.","chicago":"Song, Youngju, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Joachim Sammler, and Derek Dreyer. “Conditional Contextual Refinement.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2023. <a href=\"https://doi.org/10.1145/3571232\">https://doi.org/10.1145/3571232</a>.","ama":"Song Y, Cho M, Lee D, Hur C-K, Sammler MJ, Dreyer D. Conditional contextual refinement. <i>Proceedings of the ACM on Programming Languages</i>. 2023;7(POPL):1121-1151. doi:<a href=\"https://doi.org/10.1145/3571232\">10.1145/3571232</a>","ista":"Song Y, Cho M, Lee D, Hur C-K, Sammler MJ, Dreyer D. 2023. Conditional contextual refinement. Proceedings of the ACM on Programming Languages. 7(POPL), 1121–1151.","mla":"Song, Youngju, et al. “Conditional Contextual Refinement.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 7, no. POPL, Association for Computing Machinery, 2023, pp. 1121–51, doi:<a href=\"https://doi.org/10.1145/3571232\">10.1145/3571232</a>.","ieee":"Y. Song, M. Cho, D. Lee, C.-K. Hur, M. J. Sammler, and D. Dreyer, “Conditional contextual refinement,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 7, no. POPL. Association for Computing Machinery, pp. 1121–1151, 2023.","apa":"Song, Y., Cho, M., Lee, D., Hur, C.-K., Sammler, M. J., &#38; Dreyer, D. (2023). Conditional contextual refinement. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3571232\">https://doi.org/10.1145/3571232</a>"},"month":"01","article_processing_charge":"No","page":"1121-1151","intvolume":"         7","doi":"10.1145/3571232","fulldoi":"https://doi.org/10.1145/3571232","language":[{"iso":"eng"}],"extern":"1","date_published":"2023-01-11T00:00:00Z","abstract":[{"lang":"eng","text":"Much work in formal verification of low-level systems is based on one of two approaches: refinement or separation logic. These two approaches have complementary benefits: refinement supports the use of programs as specifications, as well as transitive composition of proofs, whereas separation logic supports conditional specifications, as well as modular ownership reasoning about shared state. A number of verification frameworks employ these techniques in tandem, but in all such cases the benefits of the two techniques remain separate. For example, in frameworks that use relational separation logic to prove contextual refinement, the relational separation logic judgment does not support transitive composition of proofs, while the contextual refinement judgment does not support conditional specifications.  \r\nIn this paper, we propose Conditional Contextual Refinement (or CCR, for short), the first verification system to not only combine refinement and separation logic in a single framework but also to truly marry them together into a unified mechanism enjoying all the benefits of refinement and separation logic simultaneously. Specifically, unlike in prior work, CCR’s refinement specifications are both conditional (with separation logic pre- and post-conditions) and transitively composable. We implement CCR in Coq and evaluate its effectiveness on a range of interesting examples."}],"publication_identifier":{"issn":["2475-1421"]},"oa_version":"Published Version","date_updated":"2024-09-10T09:03:17Z","publisher":"Association for Computing Machinery","year":"2023","volume":7,"publication_status":"published","scopus_import":"1","author":[{"full_name":"Song, Youngju","last_name":"Song","first_name":"Youngju"},{"first_name":"Minki","full_name":"Cho, Minki","last_name":"Cho"},{"full_name":"Lee, Dongjae","last_name":"Lee","first_name":"Dongjae"},{"full_name":"Hur, Chung-Kil","last_name":"Hur","first_name":"Chung-Kil"},{"id":"510d3901-2a03-11ee-914d-d9ae9011f0a7","first_name":"Michael Joachim","full_name":"Sammler, Michael Joachim","last_name":"Sammler"},{"last_name":"Dreyer","full_name":"Dreyer, Derek","first_name":"Derek"}]},{"fulldoi":"https://doi.org/10.1145/3571220","language":[{"iso":"eng"}],"extern":"1","date_published":"2023-01-11T00:00:00Z","abstract":[{"lang":"eng","text":"Prior work on multi-language program verification has achieved impressive results, including the compositional verification of complex compilers. But the existing approaches to this problem impose a variety of restrictions on the overall structure of multi-language programs (e.g. fixing the source language, fixing the set of involved languages, fixing the memory model, or fixing the semantics of interoperation). In this paper, we explore the problem of how to avoid such global restrictions.\r\nConcretely, we present DimSum: a new, decentralized approach to multi-language semantics and verification, which we have implemented in the Coq proof assistant. Decentralization means that we can define and reason about languages independently from each other (as independent modules communicating via events), but also combine and translate between them when necessary (via a library of combinators).\r\nWe apply DimSum to a high-level imperative language Rec (with an abstract memory model and function calls), a low-level assembly language Asm (with a concrete memory model, arbitrary jumps, and syscalls), and a mathematical specification language Spec. We evaluate DimSum on two case studies: an Asm library extending Rec with support for pointer comparison, and a coroutine library for Rec written in Asm. In both cases, we show how DimSum allows the Asm libraries to be abstracted to Rec-level specifications, despite the behavior of the Asm libraries not being syntactically expressible in Rec itself. We also verify an optimizing multi-pass compiler from Rec to Asm, showing that it is compatible with these Asm libraries."}],"publication_identifier":{"issn":["2475-1421"]},"oa_version":"Published Version","date_updated":"2024-09-10T09:13:02Z","publisher":"Association for Computing Machinery","year":"2023","volume":7,"publication_status":"published","scopus_import":"1","author":[{"last_name":"Sammler","full_name":"Sammler, Michael Joachim","id":"510d3901-2a03-11ee-914d-d9ae9011f0a7","first_name":"Michael Joachim"},{"last_name":"Spies","full_name":"Spies, Simon","first_name":"Simon"},{"first_name":"Youngju","full_name":"Song, Youngju","last_name":"Song"},{"last_name":"D'Osualdo","full_name":"D'Osualdo, Emanuele","first_name":"Emanuele"},{"last_name":"Krebbers","full_name":"Krebbers, Robbert","first_name":"Robbert"},{"first_name":"Deepak","last_name":"Garg","full_name":"Garg, Deepak"},{"last_name":"Dreyer","full_name":"Dreyer, Derek","first_name":"Derek"}],"title":"DimSum: A decentralized approach to multi-language semantics and verification","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1145/3571220"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","quality_controlled":"1","article_type":"original","day":"11","oa":1,"date_created":"2024-09-05T08:24:06Z","publication":"Proceedings of the ACM on Programming Languages","_id":"17500","type":"journal_article","issue":"POPL","citation":{"ieee":"M. J. Sammler <i>et al.</i>, “DimSum: A decentralized approach to multi-language semantics and verification,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 7, no. POPL. Association for Computing Machinery, pp. 775–805, 2023.","mla":"Sammler, Michael Joachim, et al. “DimSum: A Decentralized Approach to Multi-Language Semantics and Verification.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 7, no. POPL, Association for Computing Machinery, 2023, pp. 775–805, doi:<a href=\"https://doi.org/10.1145/3571220\">10.1145/3571220</a>.","apa":"Sammler, M. J., Spies, S., Song, Y., D’Osualdo, E., Krebbers, R., Garg, D., &#38; Dreyer, D. (2023). DimSum: A decentralized approach to multi-language semantics and verification. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3571220\">https://doi.org/10.1145/3571220</a>","short":"M.J. Sammler, S. Spies, Y. Song, E. D’Osualdo, R. Krebbers, D. Garg, D. Dreyer, Proceedings of the ACM on Programming Languages 7 (2023) 775–805.","chicago":"Sammler, Michael Joachim, Simon Spies, Youngju Song, Emanuele D’Osualdo, Robbert Krebbers, Deepak Garg, and Derek Dreyer. “DimSum: A Decentralized Approach to Multi-Language Semantics and Verification.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2023. <a href=\"https://doi.org/10.1145/3571220\">https://doi.org/10.1145/3571220</a>.","ama":"Sammler MJ, Spies S, Song Y, et al. DimSum: A decentralized approach to multi-language semantics and verification. <i>Proceedings of the ACM on Programming Languages</i>. 2023;7(POPL):775-805. doi:<a href=\"https://doi.org/10.1145/3571220\">10.1145/3571220</a>","ista":"Sammler MJ, Spies S, Song Y, D’Osualdo E, Krebbers R, Garg D, Dreyer D. 2023. DimSum: A decentralized approach to multi-language semantics and verification. Proceedings of the ACM on Programming Languages. 7(POPL), 775–805."},"status":"public","month":"01","article_processing_charge":"No","page":"775-805","doi":"10.1145/3571220","intvolume":"         7"},{"page":"1613-1638","doi":"10.1145/3563345","intvolume":"         6","article_processing_charge":"No","citation":{"ieee":"F. Zhu, M. J. Sammler, R. Lepigre, D. Dreyer, and D. Garg, “BFF: Foundational and automated verification of bitfield-manipulating programs,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 6, no. OOPSLA2. Association for Computing Machinery, pp. 1613–1638, 2022.","mla":"Zhu, Fengmin, et al. “BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 6, no. OOPSLA2, Association for Computing Machinery, 2022, pp. 1613–38, doi:<a href=\"https://doi.org/10.1145/3563345\">10.1145/3563345</a>.","apa":"Zhu, F., Sammler, M. J., Lepigre, R., Dreyer, D., &#38; Garg, D. (2022). BFF: Foundational and automated verification of bitfield-manipulating programs. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3563345\">https://doi.org/10.1145/3563345</a>","chicago":"Zhu, Fengmin, Michael Joachim Sammler, Rodolphe Lepigre, Derek Dreyer, and Deepak Garg. “BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2022. <a href=\"https://doi.org/10.1145/3563345\">https://doi.org/10.1145/3563345</a>.","short":"F. Zhu, M.J. Sammler, R. Lepigre, D. Dreyer, D. Garg, Proceedings of the ACM on Programming Languages 6 (2022) 1613–1638.","ama":"Zhu F, Sammler MJ, Lepigre R, Dreyer D, Garg D. BFF: Foundational and automated verification of bitfield-manipulating programs. <i>Proceedings of the ACM on Programming Languages</i>. 2022;6(OOPSLA2):1613-1638. doi:<a href=\"https://doi.org/10.1145/3563345\">10.1145/3563345</a>","ista":"Zhu F, Sammler MJ, Lepigre R, Dreyer D, Garg D. 2022. BFF: Foundational and automated verification of bitfield-manipulating programs. Proceedings of the ACM on Programming Languages. 6(OOPSLA2), 1613–1638."},"status":"public","month":"10","issue":"OOPSLA2","type":"journal_article","date_created":"2024-09-05T08:27:17Z","publication":"Proceedings of the ACM on Programming Languages","_id":"17501","article_type":"original","quality_controlled":"1","day":"31","oa":1,"title":"BFF: Foundational and automated verification of bitfield-manipulating programs","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1145/3563345"}],"scopus_import":"1","author":[{"first_name":"Fengmin","full_name":"Zhu, Fengmin","last_name":"Zhu"},{"first_name":"Michael Joachim","id":"510d3901-2a03-11ee-914d-d9ae9011f0a7","last_name":"Sammler","full_name":"Sammler, Michael Joachim"},{"first_name":"Rodolphe","last_name":"Lepigre","full_name":"Lepigre, Rodolphe"},{"full_name":"Dreyer, Derek","last_name":"Dreyer","first_name":"Derek"},{"full_name":"Garg, Deepak","last_name":"Garg","first_name":"Deepak"}],"publication_status":"published","year":"2022","volume":6,"date_updated":"2024-09-10T09:49:18Z","publisher":"Association for Computing Machinery","oa_version":"Published Version","publication_identifier":{"issn":["2475-1421"]},"abstract":[{"lang":"eng","text":"Low-level systems code often needs to interact with data, such as page table entries or network packet headers, in which multiple pieces of information are packaged together as bitfield components of a single machine integer and accessed via bitfield manipulations (e.g., shifts and masking). Most existing approaches to verifying such code employ SMT solvers, instantiated with theories for bit vector reasoning: these provide a powerful hammer, but also significantly increase the trusted computing base of the verification toolchain.\r\nIn this work, we propose an alternative approach to the verification of bitfield-manipulating systems code, which we call BFF. Building on the RefinedC framework, BFF is not only highly automated (as SMT-based approaches are) but also foundational---i.e., it produces a machine-checked proof of program correctness against a formal semantics for C programs, fully mechanized in Coq. Unlike SMT-based approaches, we do not try to solve the general problem of arbitrary bit vector reasoning, but rather observe that real systems code typically accesses bitfields using simple, well-understood programming patterns: the layout of a bit vector is known up front, and its bitfields are accessed in predictable ways through a handful of bitwise operations involving bit masks. Correspondingly, we center our approach around the concept of a structured bit vector---i.e., a bit vector with a known bitfield layout---which we use to drive simple and predictable automation. We validate the BFF approach by verifying a range of bitfield-manipulating C functions drawn from real systems code, including page table manipulation code from the Linux kernel and the pKVM hypervisor."}],"extern":"1","date_published":"2022-10-31T00:00:00Z","language":[{"iso":"eng"}],"fulldoi":"https://doi.org/10.1145/3563345"},{"type":"conference","oa_version":"Published Version","citation":{"ieee":"M. J. Sammler <i>et al.</i>, “Islaris: Verification of machine code against authoritative ISA semantics,” in <i>Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, San Diego, CA, United States, 2022, pp. 825–840.","mla":"Sammler, Michael Joachim, et al. “Islaris: Verification of Machine Code against Authoritative ISA Semantics.” <i>Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, Association for Computing Machinery, 2022, pp. 825–40, doi:<a href=\"https://doi.org/10.1145/3519939.3523434\">10.1145/3519939.3523434</a>.","apa":"Sammler, M. J., Hammond, A., Lepigre, R., Campbell, B., Pichon-Pharabod, J., Dreyer, D., … Sewell, P. (2022). Islaris: Verification of machine code against authoritative ISA semantics. In <i>Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i> (pp. 825–840). San Diego, CA, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3519939.3523434\">https://doi.org/10.1145/3519939.3523434</a>","chicago":"Sammler, Michael Joachim, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, and Peter Sewell. “Islaris: Verification of Machine Code against Authoritative ISA Semantics.” In <i>Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, 825–40. Association for Computing Machinery, 2022. <a href=\"https://doi.org/10.1145/3519939.3523434\">https://doi.org/10.1145/3519939.3523434</a>.","short":"M.J. Sammler, A. Hammond, R. Lepigre, B. Campbell, J. Pichon-Pharabod, D. Dreyer, D. Garg, P. Sewell, in:, Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2022, pp. 825–840.","ista":"Sammler MJ, Hammond A, Lepigre R, Campbell B, Pichon-Pharabod J, Dreyer D, Garg D, Sewell P. 2022. Islaris: Verification of machine code against authoritative ISA semantics. Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Conference on Programming Language Design and Implementation, 825–840.","ama":"Sammler MJ, Hammond A, Lepigre R, et al. Islaris: Verification of machine code against authoritative ISA semantics. In: <i>Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>. Association for Computing Machinery; 2022:825-840. doi:<a href=\"https://doi.org/10.1145/3519939.3523434\">10.1145/3519939.3523434</a>"},"month":"06","status":"public","date_updated":"2024-09-10T11:08:03Z","publisher":"Association for Computing Machinery","year":"2022","article_processing_charge":"No","page":"825-840","doi":"10.1145/3519939.3523434","publication_status":"published","scopus_import":"1","author":[{"last_name":"Sammler","full_name":"Sammler, Michael Joachim","first_name":"Michael Joachim","id":"510d3901-2a03-11ee-914d-d9ae9011f0a7"},{"first_name":"Angus","last_name":"Hammond","full_name":"Hammond, Angus"},{"first_name":"Rodolphe","full_name":"Lepigre, Rodolphe","last_name":"Lepigre"},{"first_name":"Brian","last_name":"Campbell","full_name":"Campbell, Brian"},{"first_name":"Jean","last_name":"Pichon-Pharabod","full_name":"Pichon-Pharabod, Jean"},{"full_name":"Dreyer, Derek","last_name":"Dreyer","first_name":"Derek"},{"first_name":"Deepak","full_name":"Garg, Deepak","last_name":"Garg"},{"last_name":"Sewell","full_name":"Sewell, Peter","first_name":"Peter"}],"main_file_link":[{"url":"https://doi.org/10.1145/3519939.3523434","open_access":"1"}],"title":"Islaris: Verification of machine code against authoritative ISA semantics","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","fulldoi":"https://doi.org/10.1145/3519939.3523434","conference":{"start_date":"2022-06-13","end_date":"2022-06-17","location":"San Diego, CA, United States","name":"PLDI: Conference on Programming Language Design and Implementation"},"language":[{"iso":"eng"}],"quality_controlled":"1","day":"09","oa":1,"extern":"1","date_published":"2022-06-09T00:00:00Z","date_created":"2024-09-05T08:29:08Z","_id":"17502","abstract":[{"text":"Recent years have seen great advances towards verifying large-scale systems code. However, these verifications are usually based on hand-written assembly or machine-code semantics for the underlying architecture that only cover a small part of the instruction set architecture (ISA). In contrast, other recent work has used Sail to establish formal models for large real-world architectures, including Armv8-A and RISC-V, that are comprehensive (complete enough to boot an operating system or hypervisor) and authoritative (automatically derived from the Arm internal model and validated against the Arm validation suite, and adopted as the official formal specification by RISC-V International, respectively). But the scale and complexity of these models makes them challenging to use as a basis for verification.\r\nIn this paper, we propose Islaris, the first system to support verification of machine code above these complete and authoritative real-world ISA specifications. Islaris uses a novel combination of SMT-solver-based symbolic execution (the Isla symbolic executor) and automated reasoning in a foundational program logic (a new separation logic we derive using Iris in Coq). We show that this approach can handle Armv8-A and RISC-V machine code exercising a wide range of systems features, including installing and calling exception vectors, code parametric on a relocation address offset (from the production pKVM hypervisor); unaligned access faults; memory-mapped IO; and compiled C code using inline assembly and function pointers.","lang":"eng"}],"publication":"Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation"},{"citation":{"ista":"Lepigre R, Sammler MJ, Memarian K, Krebbers R, Dreyer D, Sewell P. 2022. VIP: Verifying real-world C idioms with integer-pointer casts. Proceedings of the ACM on Programming Languages. 6(POPL), 1–32.","ama":"Lepigre R, Sammler MJ, Memarian K, Krebbers R, Dreyer D, Sewell P. VIP: Verifying real-world C idioms with integer-pointer casts. <i>Proceedings of the ACM on Programming Languages</i>. 2022;6(POPL):1-32. doi:<a href=\"https://doi.org/10.1145/3498681\">10.1145/3498681</a>","chicago":"Lepigre, Rodolphe, Michael Joachim Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, and Peter Sewell. “VIP: Verifying Real-World C Idioms with Integer-Pointer Casts.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2022. <a href=\"https://doi.org/10.1145/3498681\">https://doi.org/10.1145/3498681</a>.","short":"R. Lepigre, M.J. Sammler, K. Memarian, R. Krebbers, D. Dreyer, P. Sewell, Proceedings of the ACM on Programming Languages 6 (2022) 1–32.","apa":"Lepigre, R., Sammler, M. J., Memarian, K., Krebbers, R., Dreyer, D., &#38; Sewell, P. (2022). VIP: Verifying real-world C idioms with integer-pointer casts. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3498681\">https://doi.org/10.1145/3498681</a>","ieee":"R. Lepigre, M. J. Sammler, K. Memarian, R. Krebbers, D. Dreyer, and P. Sewell, “VIP: Verifying real-world C idioms with integer-pointer casts,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 6, no. POPL. Association for Computing Machinery, pp. 1–32, 2022.","mla":"Lepigre, Rodolphe, et al. “VIP: Verifying Real-World C Idioms with Integer-Pointer Casts.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 6, no. POPL, Association for Computing Machinery, 2022, pp. 1–32, doi:<a href=\"https://doi.org/10.1145/3498681\">10.1145/3498681</a>."},"status":"public","month":"01","issue":"POPL","type":"journal_article","page":"1-32","doi":"10.1145/3498681","intvolume":"         6","article_processing_charge":"No","title":"VIP: Verifying real-world C idioms with integer-pointer casts","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","main_file_link":[{"url":"https://doi.org/10.1145/3498681","open_access":"1"}],"date_created":"2024-09-05T08:31:09Z","_id":"17503","publication":"Proceedings of the ACM on Programming Languages","quality_controlled":"1","article_type":"original","day":"12","oa":1,"oa_version":"Published Version","publication_identifier":{"issn":["2475-1421"]},"scopus_import":"1","author":[{"last_name":"Lepigre","full_name":"Lepigre, Rodolphe","first_name":"Rodolphe"},{"last_name":"Sammler","full_name":"Sammler, Michael Joachim","id":"510d3901-2a03-11ee-914d-d9ae9011f0a7","first_name":"Michael Joachim"},{"last_name":"Memarian","full_name":"Memarian, Kayvan","first_name":"Kayvan"},{"last_name":"Krebbers","full_name":"Krebbers, Robbert","first_name":"Robbert"},{"last_name":"Dreyer","full_name":"Dreyer, Derek","first_name":"Derek"},{"full_name":"Sewell, Peter","last_name":"Sewell","first_name":"Peter"}],"publication_status":"published","year":"2022","volume":6,"date_updated":"2024-09-10T09:48:57Z","publisher":"Association for Computing Machinery","abstract":[{"lang":"eng","text":"Systems code often requires fine-grained control over memory layout and pointers, expressed using low-level (e.g., bitwise) operations on pointer values. Since these operations go beyond what basic pointer arithmetic in C allows, they are performed with the help of integer-pointer casts. Prior work has explored increasingly realistic memory object models for C that account for the desired semantics of integer-pointer casts while also being sound w.r.t. compiler optimisations, culminating in PNVI, the preferred memory object model in ongoing discussions within the ISO WG14 C standards committee. However, its complexity makes it an unappealing target for verification, and no tools currently exist to verify C programs under PNVI.\r\nIn this paper, we introduce VIP, a new memory object model aimed at supporting C verification. VIP sidesteps the complexities of PNVI with a simple but effective idea: a new construct that lets programmers express the intended provenances of integer-pointer casts explicitly. At the same time, we prove VIP compatible with PNVI, thus enabling verification on top of VIP to benefit from PNVI’s validation with respect to practice. In particular, we build a verification tool, RefinedC-VIP, for verifying programs under VIP semantics. As the name suggests, RefinedC-VIP extends the recently developed RefinedC tool, which is automated yet also produces foundational proofs in Coq. We evaluate RefinedC-VIP on a range of systems-code idioms, and validate VIP’s expressiveness via an implementation in the Cerberus C semantics."}],"extern":"1","date_published":"2022-01-12T00:00:00Z","language":[{"iso":"eng"}],"fulldoi":"https://doi.org/10.1145/3498681"},{"language":[{"iso":"eng"}],"fulldoi":"https://doi.org/10.1145/3498689","abstract":[{"text":"Today’s compilers employ a variety of non-trivial optimizations to achieve good performance. One key trick compilers use to justify transformations of concurrent programs is to assume that the source program has no data races: if it does, they cause the program to have undefined behavior (UB) and give the compiler free rein. However, verifying correctness of optimizations that exploit this assumption is a non-trivial problem. In particular, prior work either has not proven that such optimizations preserve program termination (particularly non-obvious when considering optimizations that move instructions out of loop bodies), or has treated all synchronization operations as external functions (losing the ability to reorder instructions around them).\r\nIn this work we present Simuliris, the first simulation technique to establish termination preservation (under a fair scheduler) for a range of concurrent program transformations that exploit UB in the source language. Simuliris is based on the idea of using ownership to reason modularly about the assumptions the compiler makes about programs with well-defined behavior. This brings the benefits of concurrent separation logics to the space of verifying program transformations: we can combine powerful reasoning techniques such as framing and coinduction to perform thread-local proofs of non-trivial concurrent program optimizations. Simuliris is built on a (non-step-indexed) variant of the Coq-based Iris framework, and is thus not tied to a particular language. In addition to demonstrating the effectiveness of Simuliris on standard compiler optimizations involving data race UB, we also instantiate it with Jung et al.’s Stacked Borrows semantics for Rust and generalize their proofs of interesting type-based aliasing optimizations to account for concurrency.","lang":"eng"}],"date_published":"2022-01-12T00:00:00Z","extern":"1","volume":6,"year":"2022","publisher":"Association for Computing Machinery","date_updated":"2024-09-10T09:48:37Z","author":[{"last_name":"Gäher","full_name":"Gäher, Lennard","first_name":"Lennard"},{"id":"510d3901-2a03-11ee-914d-d9ae9011f0a7","first_name":"Michael Joachim","full_name":"Sammler, Michael Joachim","last_name":"Sammler"},{"full_name":"Spies, Simon","last_name":"Spies","first_name":"Simon"},{"first_name":"Ralf","last_name":"Jung","full_name":"Jung, Ralf"},{"first_name":"Hoang-Hai","full_name":"Dang, Hoang-Hai","last_name":"Dang"},{"last_name":"Krebbers","full_name":"Krebbers, Robbert","first_name":"Robbert"},{"first_name":"Jeehoon","full_name":"Kang, Jeehoon","last_name":"Kang"},{"full_name":"Dreyer, Derek","last_name":"Dreyer","first_name":"Derek"}],"scopus_import":"1","publication_status":"published","publication_identifier":{"issn":["2475-1421"]},"oa_version":"Published Version","oa":1,"day":"12","quality_controlled":"1","article_type":"original","_id":"17504","publication":"Proceedings of the ACM on Programming Languages","date_created":"2024-09-05T08:32:16Z","title":"Simuliris: A separation logic framework for verifying concurrent program optimizations","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1145/3498689"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","article_processing_charge":"No","intvolume":"         6","doi":"10.1145/3498689","page":"1-31","type":"journal_article","issue":"POPL","citation":{"short":"L. Gäher, M.J. Sammler, S. Spies, R. Jung, H.-H. Dang, R. Krebbers, J. Kang, D. Dreyer, Proceedings of the ACM on Programming Languages 6 (2022) 1–31.","chicago":"Gäher, Lennard, Michael Joachim Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer. “Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2022. <a href=\"https://doi.org/10.1145/3498689\">https://doi.org/10.1145/3498689</a>.","ista":"Gäher L, Sammler MJ, Spies S, Jung R, Dang H-H, Krebbers R, Kang J, Dreyer D. 2022. Simuliris: A separation logic framework for verifying concurrent program optimizations. Proceedings of the ACM on Programming Languages. 6(POPL), 1–31.","ama":"Gäher L, Sammler MJ, Spies S, et al. Simuliris: A separation logic framework for verifying concurrent program optimizations. <i>Proceedings of the ACM on Programming Languages</i>. 2022;6(POPL):1-31. doi:<a href=\"https://doi.org/10.1145/3498689\">10.1145/3498689</a>","ieee":"L. Gäher <i>et al.</i>, “Simuliris: A separation logic framework for verifying concurrent program optimizations,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 6, no. POPL. Association for Computing Machinery, pp. 1–31, 2022.","mla":"Gäher, Lennard, et al. “Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 6, no. POPL, Association for Computing Machinery, 2022, pp. 1–31, doi:<a href=\"https://doi.org/10.1145/3498689\">10.1145/3498689</a>.","apa":"Gäher, L., Sammler, M. J., Spies, S., Jung, R., Dang, H.-H., Krebbers, R., … Dreyer, D. (2022). Simuliris: A separation logic framework for verifying concurrent program optimizations. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3498689\">https://doi.org/10.1145/3498689</a>"},"status":"public","month":"01"},{"fulldoi":"https://doi.org/10.1145/3453483.3454036","conference":{"start_date":"2021-06-20","name":"PLDI: Conference on Programming Language Design and Implementation","location":"virtual","end_date":"2021-06-25"},"day":"18","language":[{"iso":"eng"}],"quality_controlled":"1","oa":1,"extern":"1","date_published":"2021-06-18T00:00:00Z","date_created":"2024-09-05T08:34:50Z","abstract":[{"lang":"eng","text":"Given the central role that C continues to play in systems software, and the difficulty of writing safe and correct C code, it remains a grand challenge to develop effective formal methods for verifying C programs. In this paper, we propose a new approach to this problem: a type system we call RefinedC, which combines ownership types (for modular reasoning about shared state and concurrency) with refinement types (for encoding precise invariants on C data types and Hoare-style specifications for C functions).\r\nRefinedC is both automated (requiring minimal user intervention) and foundational (producing a proof of program correctness in Coq), while at the same time handling a range of low-level programming idioms such as pointer arithmetic. In particular, following the approach of RustBelt, the soundness of the RefinedC type system is justified semantically by interpretation into the Coq-based Iris framework for higher-order concurrent separation logic. However, the typing rules of RefinedC are also designed to be encodable in a new “separation logic programming” language we call Lithium. By restricting to a carefully chosen (yet expressive) fragment of separation logic, Lithium supports predictable, automatic, goal-directed proof search without backtracking. We demonstrate the effectiveness of RefinedC on a range of representative examples of C code."}],"_id":"17505","publication":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","title":"RefinedC: Automating the foundational verification of C code with refined ownership types","main_file_link":[{"url":"https://doi.org/10.1145/3453483.3454036","open_access":"1"}],"date_updated":"2024-09-10T11:54:22Z","publisher":"Association for Computing Machinery","year":"2021","article_processing_charge":"No","page":"158-174","doi":"10.1145/3453483.3454036","publication_status":"published","scopus_import":"1","author":[{"first_name":"Michael Joachim","id":"510d3901-2a03-11ee-914d-d9ae9011f0a7","full_name":"Sammler, Michael Joachim","last_name":"Sammler"},{"full_name":"Lepigre, Rodolphe","last_name":"Lepigre","first_name":"Rodolphe"},{"first_name":"Robbert","last_name":"Krebbers","full_name":"Krebbers, Robbert"},{"last_name":"Memarian","full_name":"Memarian, Kayvan","first_name":"Kayvan"},{"first_name":"Derek","last_name":"Dreyer","full_name":"Dreyer, Derek"},{"full_name":"Garg, Deepak","last_name":"Garg","first_name":"Deepak"}],"type":"conference","oa_version":"Published Version","month":"06","status":"public","citation":{"apa":"Sammler, M. J., Lepigre, R., Krebbers, R., Memarian, K., Dreyer, D., &#38; Garg, D. (2021). RefinedC: Automating the foundational verification of C code with refined ownership types. In <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i> (pp. 158–174). virtual: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3453483.3454036\">https://doi.org/10.1145/3453483.3454036</a>","ieee":"M. J. Sammler, R. Lepigre, R. Krebbers, K. Memarian, D. Dreyer, and D. Garg, “RefinedC: Automating the foundational verification of C code with refined ownership types,” in <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, virtual, 2021, pp. 158–174.","mla":"Sammler, Michael Joachim, et al. “RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types.” <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, Association for Computing Machinery, 2021, pp. 158–74, doi:<a href=\"https://doi.org/10.1145/3453483.3454036\">10.1145/3453483.3454036</a>.","ista":"Sammler MJ, Lepigre R, Krebbers R, Memarian K, Dreyer D, Garg D. 2021. RefinedC: Automating the foundational verification of C code with refined ownership types. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Conference on Programming Language Design and Implementation, 158–174.","ama":"Sammler MJ, Lepigre R, Krebbers R, Memarian K, Dreyer D, Garg D. RefinedC: Automating the foundational verification of C code with refined ownership types. In: <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>. Association for Computing Machinery; 2021:158-174. doi:<a href=\"https://doi.org/10.1145/3453483.3454036\">10.1145/3453483.3454036</a>","short":"M.J. Sammler, R. Lepigre, R. Krebbers, K. Memarian, D. Dreyer, D. Garg, in:, Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2021, pp. 158–174.","chicago":"Sammler, Michael Joachim, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, and Deepak Garg. “RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types.” In <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, 158–74. Association for Computing Machinery, 2021. <a href=\"https://doi.org/10.1145/3453483.3454036\">https://doi.org/10.1145/3453483.3454036</a>."}},{"language":[{"iso":"eng"}],"fulldoi":"https://doi.org/10.1145/3371100","abstract":[{"text":"Sandboxing is a common technique that allows low-level, untrusted components to safely interact with trusted code. However, previous work has only investigated the low-level memory isolation guarantees of sandboxing, leaving open the question of the end-to-end guarantees that sandboxing affords programmers. In this paper, we fill this gap by showing that sandboxing enables reasoning about the known concept of robust safety, i.e., safety of the trusted code even in the presence of arbitrary untrusted code. To do this, we first present an idealized operational semantics for a language that combines trusted code with untrusted code. Sandboxing is built into our semantics. Then, we prove that safety properties of the trusted code (as enforced through a rich type system) are upheld in the presence of arbitrary untrusted code, so long as all interactions with untrusted code occur at the “any” type (a type inhabited by all values). Finally, to alleviate the burden of having to interact with untrusted code at only the “any” type, we formalize and prove safe several wrappers, which automatically convert values between the “any” type and much richer types. All our results are mechanized in the Coq proof assistant.","lang":"eng"}],"date_published":"2019-12-20T00:00:00Z","extern":"1","volume":4,"year":"2019","publisher":"Association for Computing Machinery","date_updated":"2024-09-10T09:58:57Z","author":[{"first_name":"Michael Joachim","id":"510d3901-2a03-11ee-914d-d9ae9011f0a7","full_name":"Sammler, Michael Joachim","last_name":"Sammler"},{"last_name":"Garg","full_name":"Garg, Deepak","first_name":"Deepak"},{"full_name":"Dreyer, Derek","last_name":"Dreyer","first_name":"Derek"},{"last_name":"Litak","full_name":"Litak, Tadeusz","first_name":"Tadeusz"}],"scopus_import":"1","publication_status":"published","publication_identifier":{"issn":["2475-1421"]},"oa_version":"Published Version","oa":1,"day":"20","article_type":"original","quality_controlled":"1","_id":"17506","publication":"Proceedings of the ACM on Programming Languages","date_created":"2024-09-05T08:36:52Z","title":"The high-level benefits of low-level sandboxing","main_file_link":[{"url":"https://doi.org/10.1145/3371100","open_access":"1"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","article_processing_charge":"No","intvolume":"         4","doi":"10.1145/3371100","page":"1-32","issue":"POPL","type":"journal_article","citation":{"ista":"Sammler MJ, Garg D, Dreyer D, Litak T. 2019. The high-level benefits of low-level sandboxing. Proceedings of the ACM on Programming Languages. 4(POPL), 1–32.","ama":"Sammler MJ, Garg D, Dreyer D, Litak T. The high-level benefits of low-level sandboxing. <i>Proceedings of the ACM on Programming Languages</i>. 2019;4(POPL):1-32. doi:<a href=\"https://doi.org/10.1145/3371100\">10.1145/3371100</a>","short":"M.J. Sammler, D. Garg, D. Dreyer, T. Litak, Proceedings of the ACM on Programming Languages 4 (2019) 1–32.","chicago":"Sammler, Michael Joachim, Deepak Garg, Derek Dreyer, and Tadeusz Litak. “The High-Level Benefits of Low-Level Sandboxing.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2019. <a href=\"https://doi.org/10.1145/3371100\">https://doi.org/10.1145/3371100</a>.","apa":"Sammler, M. J., Garg, D., Dreyer, D., &#38; Litak, T. (2019). The high-level benefits of low-level sandboxing. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3371100\">https://doi.org/10.1145/3371100</a>","mla":"Sammler, Michael Joachim, et al. “The High-Level Benefits of Low-Level Sandboxing.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 4, no. POPL, Association for Computing Machinery, 2019, pp. 1–32, doi:<a href=\"https://doi.org/10.1145/3371100\">10.1145/3371100</a>.","ieee":"M. J. Sammler, D. Garg, D. Dreyer, and T. Litak, “The high-level benefits of low-level sandboxing,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 4, no. POPL. Association for Computing Machinery, pp. 1–32, 2019."},"status":"public","month":"12"}]