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, 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
[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. 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
[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. 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
[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. 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
[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. Conditional contextual refinement. Proceedings of the ACM on Programming Languages. 2023;7(POPL):1121-1151. doi:10.1145/3571232
[Published Version]
View
| DOI
| Download Published Version (ext.)
2023 | Published | Journal Article | IST-REx-ID: 17500 |
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
[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. 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
[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. 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
[Published Version]
View
| DOI
| Download Published Version (ext.)
2022 | Published | Journal Article | IST-REx-ID: 17504 |
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
[Published Version]
View
| DOI
| Download Published Version (ext.)
2019 | Published | Journal Article | IST-REx-ID: 17506 |
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
[Published Version]
View
| DOI
| Download Published Version (ext.)
2019 | Published | Journal Article | IST-REx-ID: 6380 |
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
[Published Version]
View
| Files available
| DOI