[{"file_date_updated":"2026-02-12T13:51:03Z","license":"https://creativecommons.org/licenses/by/4.0/","article_type":"original","day":"08","volume":10,"year":"2026","file":[{"checksum":"79be391061efbf9542638996959ce11a","access_level":"open_access","date_updated":"2026-02-12T13:51:03Z","creator":"dernst","content_type":"application/pdf","file_name":"2026_ProcACMProgrammingLanguages_Mueck.pdf","relation":"main_file","date_created":"2026-02-12T13:51:03Z","file_id":"21221","file_size":1058876,"success":1}],"type":"journal_article","publication_status":"published","has_accepted_license":"1","date_updated":"2026-02-12T13:53:04Z","title":"Endangered by the language but saved by the compiler: Robust safety via semantic back-translation","department":[{"_id":"MiSa"}],"article_processing_charge":"Yes (via OA deal)","quality_controlled":"1","author":[{"first_name":"Niklas","full_name":"Mück, Niklas","last_name":"Mück"},{"first_name":"Aïna Linn","full_name":"Georges, Aïna Linn","last_name":"Georges"},{"last_name":"Dreyer","full_name":"Dreyer, Derek","first_name":"Derek"},{"last_name":"Garg","first_name":"Deepak","full_name":"Garg, Deepak"},{"first_name":"Michael Joachim","full_name":"Sammler, Michael Joachim","last_name":"Sammler","id":"510d3901-2a03-11ee-914d-d9ae9011f0a7"}],"PlanS_conform":"1","publisher":"Association for Computing Machinery","ddc":["000"],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2026-01-08T00:00:00Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"publication_identifier":{"eissn":["2475-1421"]},"citation":{"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.","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>.","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>","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.","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>.","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>"},"doi":"10.1145/3776682","oa_version":"Published Version","OA_type":"hybrid","intvolume":"        10","_id":"21041","language":[{"iso":"eng"}],"page":"1153-1182","scopus_import":"1","abstract":[{"lang":"eng","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."}],"OA_place":"publisher","oa":1,"publication":"Proceedings of the ACM on Programming Languages","month":"01","date_created":"2026-01-25T23:01:40Z"},{"conference":{"location":"Rennes, France","start_date":"2026-01-12","name":"CPP: Conference on Certified Programs and Proofs","end_date":"2026-01-13"},"file_date_updated":"2026-02-16T08:40:29Z","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.","year":"2026","day":"08","department":[{"_id":"MiSa"}],"title":"A recipe for modular verification of generic tree traversals","article_processing_charge":"No","has_accepted_license":"1","date_updated":"2026-02-16T08:43:24Z","type":"conference","publication_status":"published","file":[{"content_type":"application/pdf","creator":"dernst","file_name":"2026_CPP_Elbeheiry.pdf","relation":"main_file","date_created":"2026-02-16T08:40:29Z","file_id":"21225","success":1,"file_size":811872,"checksum":"7df99991493e907d83a197151f378e3e","access_level":"open_access","date_updated":"2026-02-16T08:40:29Z"}],"publisher":"Association for Computing Machinery","ddc":["000"],"quality_controlled":"1","author":[{"last_name":"Elbeheiry","first_name":"Laila","full_name":"Elbeheiry, Laila"},{"first_name":"Michael Joachim","full_name":"Sammler, Michael Joachim","last_name":"Sammler","id":"510d3901-2a03-11ee-914d-d9ae9011f0a7"},{"first_name":"Robbert","full_name":"Krebbers, Robbert","last_name":"Krebbers"},{"last_name":"Dreyer","first_name":"Derek","full_name":"Dreyer, Derek"},{"full_name":"Garg, Deepak","first_name":"Deepak","last_name":"Garg"}],"date_published":"2026-01-08T00:00:00Z","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_identifier":{"isbn":["9798400723414"]},"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"page":"339-352","language":[{"iso":"eng"}],"OA_type":"gold","_id":"21133","citation":{"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.","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>","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>.","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.","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>.","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."},"oa_version":"Published Version","doi":"10.1145/3779031.3779110","publication":"Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs","month":"01","date_created":"2026-02-01T23:01:43Z","oa":1,"OA_place":"publisher","scopus_import":"1","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."}]},{"language":[{"iso":"eng"}],"page":"848-873","citation":{"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>","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>.","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>","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.","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>.","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."},"doi":"10.1145/3729284","oa_version":"Published Version","OA_type":"hybrid","intvolume":"         9","corr_author":"1","_id":"19935","oa":1,"date_created":"2025-06-30T08:47:31Z","publication":"Proceedings of the ACM on Programming Languages","month":"06","scopus_import":"1","abstract":[{"lang":"eng","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."}],"OA_place":"publisher","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2025-06-01T00:00:00Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"publication_identifier":{"eissn":["2475-1421"]},"has_accepted_license":"1","issue":"PLDI","date_updated":"2025-06-30T09:10:11Z","title":"Destabilizing Iris","department":[{"_id":"MiSa"}],"article_processing_charge":"Yes (in subscription journal)","file":[{"success":1,"file_size":843343,"date_created":"2025-06-30T09:01:08Z","file_id":"19938","relation":"main_file","content_type":"application/pdf","creator":"dernst","file_name":"2025_ProcACMProg_Spies.pdf","date_updated":"2025-06-30T09:01:08Z","access_level":"open_access","checksum":"6b72d84c10a10ba7cd1646e2c36dc1ff"}],"type":"journal_article","publication_status":"published","publisher":"Association for Computing Machinery","ddc":["000"],"quality_controlled":"1","author":[{"full_name":"Spies, Simon","first_name":"Simon","last_name":"Spies"},{"last_name":"Mück","full_name":"Mück, Niklas","first_name":"Niklas"},{"first_name":"Haoyi","full_name":"Zeng, Haoyi","last_name":"Zeng"},{"last_name":"Sammler","id":"510d3901-2a03-11ee-914d-d9ae9011f0a7","first_name":"Michael Joachim","full_name":"Sammler, Michael Joachim"},{"last_name":"Lattuada","full_name":"Lattuada, Andrea","first_name":"Andrea"},{"first_name":"Peter","full_name":"Müller, Peter","last_name":"Müller"},{"last_name":"Dreyer","first_name":"Derek","full_name":"Dreyer, Derek"}],"article_type":"original","file_date_updated":"2025-06-30T09:01:08Z","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.","day":"01","volume":9,"year":"2025"},{"issue":"PLDI","has_accepted_license":"1","date_updated":"2025-06-30T09:09:55Z","title":"RefinedProsa: Connecting response-time analysis with C verification for interrupt-free schedulers","department":[{"_id":"MiSa"}],"article_processing_charge":"Yes (in subscription journal)","file":[{"date_updated":"2025-06-30T09:08:05Z","checksum":"8c18d777feb342a7265c54b16205ec4c","access_level":"open_access","date_created":"2025-06-30T09:08:05Z","file_id":"19939","success":1,"file_size":1043790,"creator":"dernst","content_type":"application/pdf","file_name":"2025_ProcACMProg_Bedarkar.pdf","relation":"main_file"}],"type":"journal_article","publication_status":"published","publisher":"Association for Computing Machinery","ddc":["000"],"quality_controlled":"1","author":[{"last_name":"Bedarkar","first_name":"Kimaya","full_name":"Bedarkar, Kimaya"},{"first_name":"Laila","full_name":"Elbeheiry, Laila","last_name":"Elbeheiry"},{"last_name":"Sammler","id":"510d3901-2a03-11ee-914d-d9ae9011f0a7","first_name":"Michael Joachim","full_name":"Sammler, Michael Joachim"},{"first_name":"Lennard","full_name":"Gäher, Lennard","last_name":"Gäher"},{"last_name":"Brandenburg","full_name":"Brandenburg, Björn","first_name":"Björn"},{"first_name":"Derek","full_name":"Dreyer, Derek","last_name":"Dreyer"},{"last_name":"Garg","first_name":"Deepak","full_name":"Garg, Deepak"}],"article_type":"original","file_date_updated":"2025-06-30T09:08:05Z","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).","day":"13","volume":9,"year":"2025","language":[{"iso":"eng"}],"page":"73-97","citation":{"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>.","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.","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.","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.","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>.","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>","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>"},"oa_version":"Published Version","doi":"10.1145/3729249","intvolume":"         9","OA_type":"hybrid","_id":"19936","corr_author":"1","oa":1,"month":"06","publication":"Proceedings of the ACM on Programming Languages","date_created":"2025-06-30T08:47:58Z","abstract":[{"lang":"eng","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."}],"scopus_import":"1","OA_place":"publisher","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2025-06-13T00:00:00Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"publication_identifier":{"issn":["2475-1421"]}}]