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