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 | 
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.
[Published Version]
View
| Files available
| DOI
2024 | Published | Journal Article | IST-REx-ID: 17495 |
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.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2024 | Published | Journal Article | IST-REx-ID: 17497 |
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.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2023 | Published | Journal Article | IST-REx-ID: 17498 |
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.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2023 | Published | Journal Article | IST-REx-ID: 17499 |
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.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2023 | Published | Journal Article | IST-REx-ID: 17500 |
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.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2022 | Published | Journal Article | IST-REx-ID: 17501 |
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.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2022 | Published | Journal Article | IST-REx-ID: 17503 |
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.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2022 | Published | Journal Article | IST-REx-ID: 17504 |
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.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2019 | Published | Journal Article | IST-REx-ID: 17506 |
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.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2019 | Published | Journal Article | IST-REx-ID: 6380 |
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.
[Published Version]
View
| Files available
| DOI