Please note that ISTA Research Explorer no longer supports Internet Explorer versions 8 or 9 (or earlier).
We recommend upgrading to the latest Internet Explorer, Google Chrome, or Firefox.
11 Publications
2025 | Published | Journal Article | IST-REx-ID: 19936 | 
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.
[Published Version]
View
| Files available
| DOI
2024 | Published | Journal Article | IST-REx-ID: 17495 |
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.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2024 | Published | Journal Article | IST-REx-ID: 17497 |
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.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2023 | Published | Journal Article | IST-REx-ID: 17498 |
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.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2023 | Published | Journal Article | IST-REx-ID: 17499 |
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.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2023 | Published | Journal Article | IST-REx-ID: 17500 |
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.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2022 | Published | Journal Article | IST-REx-ID: 17501 |
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.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2022 | Published | Journal Article | IST-REx-ID: 17503 |
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.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2022 | Published | Journal Article | IST-REx-ID: 17504 |
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.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2019 | Published | Journal Article | IST-REx-ID: 17506 |
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.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2019 | Published | Journal Article | IST-REx-ID: 6380 |
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.
[Published Version]
View
| Files available
| DOI