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