@article{21041,
  abstract     = {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.
In 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.},
  author       = {Mück, Niklas and Georges, Aïna Linn and Dreyer, Derek and Garg, Deepak and Sammler, Michael Joachim},
  issn         = {2475-1421},
  journal      = {Proceedings of the ACM on Programming Languages},
  pages        = {1153--1182},
  publisher    = {Association for Computing Machinery},
  title        = {{Endangered by the language but saved by the compiler: Robust safety via semantic back-translation}},
  doi          = {10.1145/3776682},
  volume       = {10},
  year         = {2026},
}

@inproceedings{21133,
  abstract     = {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.
In 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.
At 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.},
  author       = {Elbeheiry, Laila and Sammler, Michael Joachim and Krebbers, Robbert and Dreyer, Derek and Garg, Deepak},
  booktitle    = {Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs},
  isbn         = {9798400723414},
  location     = {Rennes, France},
  pages        = {339--352},
  publisher    = {Association for Computing Machinery},
  title        = {{A recipe for modular verification of generic tree traversals}},
  doi          = {10.1145/3779031.3779110},
  year         = {2026},
}

@article{19935,
  abstract     = {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.
In 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.},
  author       = {Spies, Simon and Mück, Niklas and Zeng, Haoyi and Sammler, Michael Joachim and Lattuada, Andrea and Müller, Peter and Dreyer, Derek},
  issn         = {2475-1421},
  journal      = {Proceedings of the ACM on Programming Languages},
  number       = {PLDI},
  pages        = {848--873},
  publisher    = {Association for Computing Machinery},
  title        = {{Destabilizing Iris}},
  doi          = {10.1145/3729284},
  volume       = {9},
  year         = {2025},
}

@article{19936,
  abstract     = {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.},
  author       = {Bedarkar, Kimaya and Elbeheiry, Laila and Sammler, Michael Joachim and Gäher, Lennard and Brandenburg, Björn and Dreyer, Derek and Garg, Deepak},
  issn         = {2475-1421},
  journal      = {Proceedings of the ACM on Programming Languages},
  number       = {PLDI},
  pages        = {73--97},
  publisher    = {Association for Computing Machinery},
  title        = {{RefinedProsa: Connecting response-time analysis with C verification for interrupt-free schedulers}},
  doi          = {10.1145/3729249},
  volume       = {9},
  year         = {2025},
}