---
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
license: https://creativecommons.org/licenses/by/4.0/
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'
...
---
OA_place: publisher
OA_type: hybrid
PlanS_conform: '1'
_id: '21052'
abstract:
- lang: eng
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."
article_processing_charge: No
article_type: original
author:
- first_name: Max
full_name: Vistrup, Max
last_name: Vistrup
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Ralf
full_name: Jung, Ralf
last_name: Jung
citation:
ama: Vistrup M, Sammler MJ, Jung R. Program logics à la Carte. Proceedings of
the ACM on Programming Languages. 2025;9(POPL):300-331. doi:10.1145/3704847
apa: Vistrup, M., Sammler, M. J., & Jung, R. (2025). Program logics à la Carte.
Proceedings of the ACM on Programming Languages. Association for Computing
Machinery. https://doi.org/10.1145/3704847
chicago: Vistrup, Max, Michael Joachim Sammler, and Ralf Jung. “Program Logics à
La Carte.” Proceedings of the ACM on Programming Languages. Association
for Computing Machinery, 2025. https://doi.org/10.1145/3704847.
ieee: M. Vistrup, M. J. Sammler, and R. Jung, “Program logics à la Carte,” Proceedings
of the ACM on Programming Languages, vol. 9, no. POPL. Association for Computing
Machinery, pp. 300–331, 2025.
ista: Vistrup M, Sammler MJ, Jung R. 2025. Program logics à la Carte. Proceedings
of the ACM on Programming Languages. 9(POPL), 300–331.
mla: Vistrup, Max, et al. “Program Logics à La Carte.” Proceedings of the ACM
on Programming Languages, vol. 9, no. POPL, Association for Computing Machinery,
2025, pp. 300–31, doi:10.1145/3704847.
short: M. Vistrup, M.J. Sammler, R. Jung, Proceedings of the ACM on Programming
Languages 9 (2025) 300–331.
date_created: 2026-01-28T06:35:47Z
date_published: 2025-01-09T00:00:00Z
date_updated: 2026-02-09T06:19:36Z
day: '09'
doi: 10.1145/3704847
extern: '1'
has_accepted_license: '1'
intvolume: ' 9'
issue: POPL
language:
- iso: eng
main_file_link:
- open_access: '1'
month: '01'
oa: 1
oa_version: Published Version
page: 300-331
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: Program logics à la Carte
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
PlanS_conform: '1'
_id: '21053'
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."
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Thibault
full_name: Dardinier, Thibault
last_name: Dardinier
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Gaurav
full_name: Parthasarathy, Gaurav
last_name: Parthasarathy
- first_name: Alexander J.
full_name: Summers, Alexander J.
last_name: Summers
- first_name: Peter
full_name: Müller, Peter
last_name: Müller
citation:
ama: Dardinier T, Sammler MJ, Parthasarathy G, Summers AJ, Müller P. Formal foundations
for translational separation logic verifiers. Proceedings of the ACM on Programming
Languages. 2025;9(POPL):569-599. doi:10.1145/3704856
apa: Dardinier, T., Sammler, M. J., Parthasarathy, G., Summers, A. J., & Müller,
P. (2025). Formal foundations for translational separation logic verifiers. Proceedings
of the ACM on Programming Languages. Association for Computing Machinery.
https://doi.org/10.1145/3704856
chicago: Dardinier, Thibault, Michael Joachim Sammler, Gaurav Parthasarathy, Alexander
J. Summers, and Peter Müller. “Formal Foundations for Translational Separation
Logic Verifiers.” Proceedings of the ACM on Programming Languages. Association
for Computing Machinery, 2025. https://doi.org/10.1145/3704856.
ieee: T. Dardinier, M. J. Sammler, G. Parthasarathy, A. J. Summers, and P. Müller,
“Formal foundations for translational separation logic verifiers,” Proceedings
of the ACM on Programming Languages, 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.
mla: Dardinier, Thibault, et al. “Formal Foundations for Translational Separation
Logic Verifiers.” Proceedings of the ACM on Programming Languages, vol.
9, no. POPL, Association for Computing Machinery, 2025, pp. 569–99, doi:10.1145/3704856.
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.
date_created: 2026-01-28T06:36:57Z
date_published: 2025-01-09T00:00:00Z
date_updated: 2026-02-09T06:25:01Z
day: '09'
ddc:
- '000'
doi: 10.1145/3704856
extern: '1'
external_id:
arxiv:
- '2407.20002'
has_accepted_license: '1'
intvolume: ' 9'
issue: POPL
language:
- iso: eng
month: '01'
oa_version: Published Version
page: 569-599
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
issn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
status: public
title: Formal foundations for translational separation logic verifiers
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'
...
---
_id: '17495'
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.
article_processing_charge: No
article_type: original
author:
- first_name: Lennard
full_name: Gäher, Lennard
last_name: Gäher
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Ralf
full_name: Jung, Ralf
last_name: Jung
- first_name: Robbert
full_name: Krebbers, Robbert
last_name: Krebbers
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
citation:
ama: 'Gäher L, Sammler MJ, Jung R, Krebbers R, Dreyer D. RefinedRust: A type system
for high-assurance verification of rust programs. Proceedings of the ACM on
Programming Languages. 2024;8(PLDI):1115-1139. doi:10.1145/3656422'
apa: 'Gäher, L., Sammler, M. J., 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. Association for Computing Machinery.
https://doi.org/10.1145/3656422'
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.” Proceedings of the ACM on Programming Languages. Association
for Computing Machinery, 2024. https://doi.org/10.1145/3656422.'
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,” Proceedings
of the ACM on Programming Languages, vol. 8, no. PLDI. Association for Computing
Machinery, pp. 1115–1139, 2024.'
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.'
mla: 'Gäher, Lennard, et al. “RefinedRust: A Type System for High-Assurance Verification
of Rust Programs.” Proceedings of the ACM on Programming Languages, vol.
8, no. PLDI, Association for Computing Machinery, 2024, pp. 1115–39, doi:10.1145/3656422.'
short: L. Gäher, M.J. Sammler, R. Jung, R. Krebbers, D. Dreyer, Proceedings of the
ACM on Programming Languages 8 (2024) 1115–1139.
date_created: 2024-09-05T07:52:27Z
date_published: 2024-06-20T00:00:00Z
date_updated: 2024-09-10T07:16:49Z
day: '20'
doi: 10.1145/3656422
extern: '1'
intvolume: ' 8'
issue: PLDI
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/3656422
month: '06'
oa: 1
oa_version: Published Version
page: 1115-1139
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: 'RefinedRust: A type system for high-assurance verification of rust programs'
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 8
year: '2024'
...
---
_id: '17497'
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.'
article_processing_charge: No
article_type: original
author:
- first_name: Simon
full_name: Spies, Simon
last_name: Spies
- first_name: Lennard
full_name: Gäher, Lennard
last_name: Gäher
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
citation:
ama: 'Spies S, Gäher L, Sammler MJ, Dreyer D. Quiver: Guided abductive inference
of separation logic specifications in coq. Proceedings of the ACM on Programming
Languages. 2024;8(PLDI):889-913. doi:10.1145/3656413'
apa: 'Spies, S., Gäher, L., Sammler, M. J., & Dreyer, D. (2024). Quiver: Guided
abductive inference of separation logic specifications in coq. Proceedings
of the ACM on Programming Languages. Association for Computing Machinery.
https://doi.org/10.1145/3656413'
chicago: 'Spies, Simon, Lennard Gäher, Michael Joachim Sammler, and Derek Dreyer.
“Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq.”
Proceedings of the ACM on Programming Languages. Association for Computing
Machinery, 2024. https://doi.org/10.1145/3656413.'
ieee: 'S. Spies, L. Gäher, M. J. Sammler, and D. Dreyer, “Quiver: Guided abductive
inference of separation logic specifications in coq,” Proceedings of the ACM
on Programming Languages, vol. 8, no. PLDI. Association for Computing Machinery,
pp. 889–913, 2024.'
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.'
mla: 'Spies, Simon, et al. “Quiver: Guided Abductive Inference of Separation Logic
Specifications in Coq.” Proceedings of the ACM on Programming Languages,
vol. 8, no. PLDI, Association for Computing Machinery, 2024, pp. 889–913, doi:10.1145/3656413.'
short: S. Spies, L. Gäher, M.J. Sammler, D. Dreyer, Proceedings of the ACM on Programming
Languages 8 (2024) 889–913.
date_created: 2024-09-05T08:10:41Z
date_published: 2024-06-20T00:00:00Z
date_updated: 2024-09-10T12:00:57Z
day: '20'
doi: 10.1145/3656413
extern: '1'
intvolume: ' 8'
issue: PLDI
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/3656413
month: '06'
oa: 1
oa_version: Published Version
page: 889-913
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: 'Quiver: Guided abductive inference of separation logic specifications in coq'
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 8
year: '2024'
...
---
_id: '17498'
abstract:
- lang: eng
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.
article_processing_charge: No
article_type: original
author:
- first_name: Armaël
full_name: Guéneau, Armaël
last_name: Guéneau
- first_name: Johannes
full_name: Hostert, Johannes
last_name: Hostert
- first_name: Simon
full_name: Spies, Simon
last_name: Spies
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Lars
full_name: Birkedal, Lars
last_name: Birkedal
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
citation:
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. Proceedings
of the ACM on Programming Languages. 2023;7(OOPSLA2):716-744. doi:10.1145/3622823'
apa: 'Guéneau, A., Hostert, J., Spies, S., Sammler, M. J., Birkedal, L., & Dreyer,
D. (2023). Melocoton: A program logic for verified interoperability between OCaml
and C. Proceedings of the ACM on Programming Languages. Association for
Computing Machinery. https://doi.org/10.1145/3622823'
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.” Proceedings of the ACM on Programming Languages.
Association for Computing Machinery, 2023. https://doi.org/10.1145/3622823.'
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,”
Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA2. Association
for Computing Machinery, pp. 716–744, 2023.'
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.'
mla: 'Guéneau, Armaël, et al. “Melocoton: A Program Logic for Verified Interoperability
between OCaml and C.” Proceedings of the ACM on Programming Languages,
vol. 7, no. OOPSLA2, Association for Computing Machinery, 2023, pp. 716–44, doi:10.1145/3622823.'
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.
date_created: 2024-09-05T08:17:10Z
date_published: 2023-10-16T00:00:00Z
date_updated: 2024-09-10T09:04:24Z
day: '16'
doi: 10.1145/3622823
extern: '1'
intvolume: ' 7'
issue: OOPSLA2
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/3622823
month: '10'
oa: 1
oa_version: Published Version
page: 716-744
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: 'Melocoton: A program logic for verified interoperability between OCaml and
C'
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 7
year: '2023'
...
---
_id: '17499'
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."
article_processing_charge: No
article_type: original
author:
- first_name: Youngju
full_name: Song, Youngju
last_name: Song
- first_name: Minki
full_name: Cho, Minki
last_name: Cho
- first_name: Dongjae
full_name: Lee, Dongjae
last_name: Lee
- first_name: Chung-Kil
full_name: Hur, Chung-Kil
last_name: Hur
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
citation:
ama: Song Y, Cho M, Lee D, Hur C-K, Sammler MJ, Dreyer D. Conditional contextual
refinement. Proceedings of the ACM on Programming Languages. 2023;7(POPL):1121-1151.
doi:10.1145/3571232
apa: Song, Y., Cho, M., Lee, D., Hur, C.-K., Sammler, M. J., & Dreyer, D. (2023).
Conditional contextual refinement. Proceedings of the ACM on Programming Languages.
Association for Computing Machinery. https://doi.org/10.1145/3571232
chicago: Song, Youngju, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Joachim Sammler,
and Derek Dreyer. “Conditional Contextual Refinement.” Proceedings of the ACM
on Programming Languages. Association for Computing Machinery, 2023. https://doi.org/10.1145/3571232.
ieee: Y. Song, M. Cho, D. Lee, C.-K. Hur, M. J. Sammler, and D. Dreyer, “Conditional
contextual refinement,” Proceedings of the ACM on Programming Languages,
vol. 7, no. POPL. Association for Computing Machinery, pp. 1121–1151, 2023.
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.” Proceedings of
the ACM on Programming Languages, vol. 7, no. POPL, Association for Computing
Machinery, 2023, pp. 1121–51, doi:10.1145/3571232.
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.
date_created: 2024-09-05T08:21:51Z
date_published: 2023-01-11T00:00:00Z
date_updated: 2024-09-10T09:03:17Z
day: '11'
doi: 10.1145/3571232
extern: '1'
intvolume: ' 7'
issue: POPL
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/3571232
month: '01'
oa: 1
oa_version: Published Version
page: 1121-1151
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: Conditional contextual refinement
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 7
year: '2023'
...
---
_id: '17500'
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."
article_processing_charge: No
article_type: original
author:
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Simon
full_name: Spies, Simon
last_name: Spies
- first_name: Youngju
full_name: Song, Youngju
last_name: Song
- first_name: Emanuele
full_name: D'Osualdo, Emanuele
last_name: D'Osualdo
- first_name: Robbert
full_name: Krebbers, Robbert
last_name: Krebbers
- first_name: Deepak
full_name: Garg, Deepak
last_name: Garg
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
citation:
ama: 'Sammler MJ, Spies S, Song Y, et al. DimSum: A decentralized approach to multi-language
semantics and verification. Proceedings of the ACM on Programming Languages.
2023;7(POPL):775-805. doi:10.1145/3571220'
apa: 'Sammler, M. J., 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. Association
for Computing Machinery. https://doi.org/10.1145/3571220'
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.” Proceedings of the ACM on Programming
Languages. Association for Computing Machinery, 2023. https://doi.org/10.1145/3571220.'
ieee: 'M. J. Sammler et al., “DimSum: A decentralized approach to multi-language
semantics and verification,” Proceedings of the ACM on Programming Languages,
vol. 7, no. POPL. Association for Computing Machinery, pp. 775–805, 2023.'
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.'
mla: 'Sammler, Michael Joachim, et al. “DimSum: A Decentralized Approach to Multi-Language
Semantics and Verification.” Proceedings of the ACM on Programming Languages,
vol. 7, no. POPL, Association for Computing Machinery, 2023, pp. 775–805, doi:10.1145/3571220.'
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.
date_created: 2024-09-05T08:24:06Z
date_published: 2023-01-11T00:00:00Z
date_updated: 2024-09-10T09:13:02Z
day: '11'
doi: 10.1145/3571220
extern: '1'
intvolume: ' 7'
issue: POPL
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/3571220
month: '01'
oa: 1
oa_version: Published Version
page: 775-805
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: 'DimSum: A decentralized approach to multi-language semantics and verification'
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 7
year: '2023'
...
---
_id: '17501'
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."
article_processing_charge: No
article_type: original
author:
- first_name: Fengmin
full_name: Zhu, Fengmin
last_name: Zhu
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Rodolphe
full_name: Lepigre, Rodolphe
last_name: Lepigre
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
- first_name: Deepak
full_name: Garg, Deepak
last_name: Garg
citation:
ama: 'Zhu F, Sammler MJ, Lepigre R, Dreyer D, Garg D. BFF: Foundational and automated
verification of bitfield-manipulating programs. Proceedings of the ACM on Programming
Languages. 2022;6(OOPSLA2):1613-1638. doi:10.1145/3563345'
apa: 'Zhu, F., Sammler, M. J., Lepigre, R., Dreyer, D., & Garg, D. (2022). BFF:
Foundational and automated verification of bitfield-manipulating programs. Proceedings
of the ACM on Programming Languages. Association for Computing Machinery.
https://doi.org/10.1145/3563345'
chicago: 'Zhu, Fengmin, Michael Joachim Sammler, Rodolphe Lepigre, Derek Dreyer,
and Deepak Garg. “BFF: Foundational and Automated Verification of Bitfield-Manipulating
Programs.” Proceedings of the ACM on Programming Languages. Association
for Computing Machinery, 2022. https://doi.org/10.1145/3563345.'
ieee: 'F. Zhu, M. J. Sammler, R. Lepigre, D. Dreyer, and D. Garg, “BFF: Foundational
and automated verification of bitfield-manipulating programs,” Proceedings
of the ACM on Programming Languages, vol. 6, no. OOPSLA2. Association for
Computing Machinery, pp. 1613–1638, 2022.'
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.'
mla: 'Zhu, Fengmin, et al. “BFF: Foundational and Automated Verification of Bitfield-Manipulating
Programs.” Proceedings of the ACM on Programming Languages, vol. 6, no.
OOPSLA2, Association for Computing Machinery, 2022, pp. 1613–38, doi:10.1145/3563345.'
short: F. Zhu, M.J. Sammler, R. Lepigre, D. Dreyer, D. Garg, Proceedings of the
ACM on Programming Languages 6 (2022) 1613–1638.
date_created: 2024-09-05T08:27:17Z
date_published: 2022-10-31T00:00:00Z
date_updated: 2024-09-10T09:49:18Z
day: '31'
doi: 10.1145/3563345
extern: '1'
intvolume: ' 6'
issue: OOPSLA2
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/3563345
month: '10'
oa: 1
oa_version: Published Version
page: 1613-1638
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: 'BFF: Foundational and automated verification of bitfield-manipulating programs'
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 6
year: '2022'
...
---
_id: '17503'
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."
article_processing_charge: No
article_type: original
author:
- first_name: Rodolphe
full_name: Lepigre, Rodolphe
last_name: Lepigre
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Kayvan
full_name: Memarian, Kayvan
last_name: Memarian
- first_name: Robbert
full_name: Krebbers, Robbert
last_name: Krebbers
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
- first_name: Peter
full_name: Sewell, Peter
last_name: Sewell
citation:
ama: 'Lepigre R, Sammler MJ, Memarian K, Krebbers R, Dreyer D, Sewell P. VIP: Verifying
real-world C idioms with integer-pointer casts. Proceedings of the ACM on Programming
Languages. 2022;6(POPL):1-32. doi:10.1145/3498681'
apa: 'Lepigre, R., Sammler, M. J., 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. Association for Computing
Machinery. https://doi.org/10.1145/3498681'
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.” Proceedings of the ACM on Programming Languages. Association for
Computing Machinery, 2022. https://doi.org/10.1145/3498681.'
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,” Proceedings
of the ACM on Programming Languages, vol. 6, no. POPL. Association for Computing
Machinery, pp. 1–32, 2022.'
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.'
mla: 'Lepigre, Rodolphe, et al. “VIP: Verifying Real-World C Idioms with Integer-Pointer
Casts.” Proceedings of the ACM on Programming Languages, vol. 6, no. POPL,
Association for Computing Machinery, 2022, pp. 1–32, doi:10.1145/3498681.'
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.
date_created: 2024-09-05T08:31:09Z
date_published: 2022-01-12T00:00:00Z
date_updated: 2024-09-10T09:48:57Z
day: '12'
doi: 10.1145/3498681
extern: '1'
intvolume: ' 6'
issue: POPL
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/3498681
month: '01'
oa: 1
oa_version: Published Version
page: 1-32
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: 'VIP: Verifying real-world C idioms with integer-pointer casts'
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 6
year: '2022'
...
---
_id: '17504'
abstract:
- lang: eng
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."
article_processing_charge: No
article_type: original
author:
- first_name: Lennard
full_name: Gäher, Lennard
last_name: Gäher
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Simon
full_name: Spies, Simon
last_name: Spies
- first_name: Ralf
full_name: Jung, Ralf
last_name: Jung
- first_name: Hoang-Hai
full_name: Dang, Hoang-Hai
last_name: Dang
- first_name: Robbert
full_name: Krebbers, Robbert
last_name: Krebbers
- first_name: Jeehoon
full_name: Kang, Jeehoon
last_name: Kang
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
citation:
ama: 'Gäher L, Sammler MJ, Spies S, et al. Simuliris: A separation logic framework
for verifying concurrent program optimizations. Proceedings of the ACM on Programming
Languages. 2022;6(POPL):1-31. doi:10.1145/3498689'
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. Proceedings of the ACM on Programming Languages.
Association for Computing Machinery. https://doi.org/10.1145/3498689'
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.” Proceedings
of the ACM on Programming Languages. Association for Computing Machinery,
2022. https://doi.org/10.1145/3498689.'
ieee: 'L. Gäher et al., “Simuliris: A separation logic framework for verifying
concurrent program optimizations,” Proceedings of the ACM on Programming Languages,
vol. 6, no. POPL. Association for Computing Machinery, pp. 1–31, 2022.'
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.'
mla: 'Gäher, Lennard, et al. “Simuliris: A Separation Logic Framework for Verifying
Concurrent Program Optimizations.” Proceedings of the ACM on Programming Languages,
vol. 6, no. POPL, Association for Computing Machinery, 2022, pp. 1–31, doi:10.1145/3498689.'
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.
date_created: 2024-09-05T08:32:16Z
date_published: 2022-01-12T00:00:00Z
date_updated: 2024-09-10T09:48:37Z
day: '12'
doi: 10.1145/3498689
extern: '1'
intvolume: ' 6'
issue: POPL
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/3498689
month: '01'
oa: 1
oa_version: Published Version
page: 1-31
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: 'Simuliris: A separation logic framework for verifying concurrent program optimizations'
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 6
year: '2022'
...
---
_id: '17506'
abstract:
- lang: eng
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.
article_processing_charge: No
article_type: original
author:
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Deepak
full_name: Garg, Deepak
last_name: Garg
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
- first_name: Tadeusz
full_name: Litak, Tadeusz
last_name: Litak
citation:
ama: Sammler MJ, Garg D, Dreyer D, Litak T. The high-level benefits of low-level
sandboxing. Proceedings of the ACM on Programming Languages. 2019;4(POPL):1-32.
doi:10.1145/3371100
apa: Sammler, M. J., Garg, D., Dreyer, D., & Litak, T. (2019). The high-level
benefits of low-level sandboxing. Proceedings of the ACM on Programming Languages.
Association for Computing Machinery. https://doi.org/10.1145/3371100
chicago: Sammler, Michael Joachim, Deepak Garg, Derek Dreyer, and Tadeusz Litak.
“The High-Level Benefits of Low-Level Sandboxing.” Proceedings of the ACM on
Programming Languages. Association for Computing Machinery, 2019. https://doi.org/10.1145/3371100.
ieee: M. J. Sammler, D. Garg, D. Dreyer, and T. Litak, “The high-level benefits
of low-level sandboxing,” Proceedings of the ACM on Programming Languages,
vol. 4, no. POPL. Association for Computing Machinery, pp. 1–32, 2019.
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.
mla: Sammler, Michael Joachim, et al. “The High-Level Benefits of Low-Level Sandboxing.”
Proceedings of the ACM on Programming Languages, vol. 4, no. POPL, Association
for Computing Machinery, 2019, pp. 1–32, doi:10.1145/3371100.
short: M.J. Sammler, D. Garg, D. Dreyer, T. Litak, Proceedings of the ACM on Programming
Languages 4 (2019) 1–32.
date_created: 2024-09-05T08:36:52Z
date_published: 2019-12-20T00:00:00Z
date_updated: 2024-09-10T09:58:57Z
day: '20'
doi: 10.1145/3371100
extern: '1'
intvolume: ' 4'
issue: POPL
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/3371100
month: '12'
oa: 1
oa_version: Published Version
page: 1-32
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: The high-level benefits of low-level sandboxing
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 4
year: '2019'
...
---
OA_place: publisher
OA_type: hybrid
_id: '6380'
abstract:
- lang: eng
text: 'There is a huge gap between the speeds of modern caches and main memories,
and therefore cache misses account for a considerable loss of efficiency in programs.
The predominant technique to address this issue has been Data Packing: data elements
that are frequently accessed within time proximity are packed into the same cache
block, thereby minimizing accesses to the main memory. We consider the algorithmic
problem of Data Packing on a two-level memory system. Given a reference sequence
R of accesses to data elements, the task is to partition the elements into cache
blocks such that the number of cache misses on R is minimized. The problem is
notoriously difficult: it is NP-hard even when the cache has size 1, and is hard
to approximate for any cache size larger than 4. Therefore, all existing techniques
for Data Packing are based on heuristics and lack theoretical guarantees. In this
work, we present the first positive theoretical results for Data Packing, along
with new and stronger negative results. We consider the problem under the lens
of the underlying access hypergraphs, which are hypergraphs of affinities between
the data elements, where the order of an access hypergraph corresponds to the
size of the affinity group. We study the problem parameterized by the treewidth
of access hypergraphs, which is a standard notion in graph theory to measure the
closeness of a graph to a tree. Our main results are as follows: We show there
is a number q* depending on the cache parameters such that (a) if the access hypergraph
of order q* has constant treewidth, then there is a linear-time algorithm for
Data Packing; (b)the Data Packing problem remains NP-hard even if the access hypergraph
of order q*-1 has constant treewidth. Thus, we establish a fine-grained dichotomy
depending on a single parameter, namely, the highest order among access hypegraphs
that have constant treewidth; and establish the optimal value q* of this parameter.
Finally, we present an experimental evaluation of a prototype implementation of
our algorithm. Our results demonstrate that, in practice, access hypergraphs of
many commonly-used algorithms have small treewidth. We compare our approach with
several state-of-the-art heuristic-based algorithms and show that our algorithm
leads to significantly fewer cache-misses. '
acknowledgement: "The research was partially supported by Vienna Science and Technology
Fund (WWTF) Project ICT15-003, Austrian Science Fund (FWF) NFN Grant No S11407-N23
(RiSE/SHiNE), ERC\r\nStarting Grant (279307: Graph Games), and the IBM PhD Fellowship
program."
article_number: '53'
article_processing_charge: Yes (in subscription journal)
article_type: original
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Amir Kafshdar
full_name: Goharshady, Amir Kafshdar
id: 391365CE-F248-11E8-B48F-1D18A9856A87
last_name: Goharshady
orcid: 0000-0003-1702-6584
- first_name: Nastaran
full_name: Okati, Nastaran
last_name: Okati
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
citation:
ama: Chatterjee K, Goharshady AK, Okati N, Pavlogiannis A. Efficient parameterized
algorithms for data packing. Proceedings of the ACM on Programming Languages.
2019;3(POPL). doi:10.1145/3290366
apa: Chatterjee, K., Goharshady, A. K., Okati, N., & Pavlogiannis, A. (2019).
Efficient parameterized algorithms for data packing. Proceedings of the ACM
on Programming Languages. ACM. https://doi.org/10.1145/3290366
chicago: Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Nastaran Okati, and Andreas
Pavlogiannis. “Efficient Parameterized Algorithms for Data Packing.” Proceedings
of the ACM on Programming Languages. ACM, 2019. https://doi.org/10.1145/3290366.
ieee: K. Chatterjee, A. K. Goharshady, N. Okati, and A. Pavlogiannis, “Efficient
parameterized algorithms for data packing,” Proceedings of the ACM on Programming
Languages, vol. 3, no. POPL. ACM, 2019.
ista: Chatterjee K, Goharshady AK, Okati N, Pavlogiannis A. 2019. Efficient parameterized
algorithms for data packing. Proceedings of the ACM on Programming Languages.
3(POPL), 53.
mla: Chatterjee, Krishnendu, et al. “Efficient Parameterized Algorithms for Data
Packing.” Proceedings of the ACM on Programming Languages, vol. 3, no.
POPL, 53, ACM, 2019, doi:10.1145/3290366.
short: K. Chatterjee, A.K. Goharshady, N. Okati, A. Pavlogiannis, Proceedings of
the ACM on Programming Languages 3 (2019).
date_created: 2019-05-06T12:18:17Z
date_published: 2019-01-01T00:00:00Z
date_updated: 2026-06-18T22:31:01Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.1145/3290366
ec_funded: 1
file:
- access_level: open_access
checksum: c157752f96877b36685ad7063ada4524
content_type: application/pdf
creator: dernst
date_created: 2019-05-06T12:23:11Z
date_updated: 2020-07-14T12:47:29Z
file_id: '6381'
file_name: 2019_ACM_POPL_Chatterjee.pdf
file_size: 1294962
relation: main_file
file_date_updated: 2020-07-14T12:47:29Z
has_accepted_license: '1'
intvolume: ' 3'
issue: POPL
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
issn:
- 2475-1421
publication_status: published
publisher: ACM
pubrep_id: '1056'
quality_controlled: '1'
related_material:
record:
- id: '8934'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Efficient parameterized algorithms for data packing
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: 3
year: '2019'
...