Michael Joachim Sammler

17 Publications

Mark all

[17]
2026 | Published | Journal Article | IST-REx-ID: 21041 | OA | PlanS
Mück, N., Georges, A. L., Dreyer, D., Garg, D., & Sammler, M. J. (2026). Endangered by the language but saved by the compiler: Robust safety via semantic back-translation. Proceedings of the ACM on Programming Languages. Association for Computing Machinery. https://doi.org/10.1145/3776682
[Published Version] View | Files available | DOI
 
[16]
2026 | Published | Conference Paper | IST-REx-ID: 21133 | OA
Elbeheiry, L., Sammler, M. J., Krebbers, R., Dreyer, D., & Garg, D. (2026). A recipe for modular verification of generic tree traversals. In Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs (pp. 339–352). Rennes, France: Association for Computing Machinery. https://doi.org/10.1145/3779031.3779110
[Published Version] View | Files available | DOI
 
[15]
2025 | Published | Journal Article | IST-REx-ID: 21052 | OA | PlanS
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
[Published Version] View | DOI | Download Published Version (ext.)
 
[14]
2025 | Published | Journal Article | IST-REx-ID: 21053 | PlanS
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
[Published Version] View | DOI | arXiv
 
[13]
2025 | Published | Journal Article | IST-REx-ID: 19935 | OA
Spies, S., Mück, N., Zeng, H., Sammler, M. J., Lattuada, A., Müller, P., & Dreyer, D. (2025). Destabilizing Iris. Proceedings of the ACM on Programming Languages. Association for Computing Machinery. https://doi.org/10.1145/3729284
[Published Version] View | Files available | DOI
 
[12]
2025 | Published | Journal Article | IST-REx-ID: 19936 | OA
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
 
[11]
2024 | Published | Journal Article | IST-REx-ID: 17495 | OA
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.)
 
[10]
2024 | Published | Journal Article | IST-REx-ID: 17497 | OA
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.)
 
[9]
2023 | Published | Journal Article | IST-REx-ID: 17498 | OA
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.)
 
[8]
2023 | Published | Journal Article | IST-REx-ID: 17499 | OA
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.)
 
[7]
2023 | Published | Journal Article | IST-REx-ID: 17500 | OA
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.)
 
[6]
2022 | Published | Journal Article | IST-REx-ID: 17501 | OA
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.)
 
[5]
2022 | Published | Conference Paper | IST-REx-ID: 17502 | OA
Sammler, M. J., Hammond, A., Lepigre, R., Campbell, B., Pichon-Pharabod, J., Dreyer, D., … Sewell, P. (2022). Islaris: Verification of machine code against authoritative ISA semantics. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (pp. 825–840). San Diego, CA, United States: Association for Computing Machinery. https://doi.org/10.1145/3519939.3523434
[Published Version] View | DOI | Download Published Version (ext.)
 
[4]
2022 | Published | Journal Article | IST-REx-ID: 17503 | OA
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.)
 
[3]
2022 | Published | Journal Article | IST-REx-ID: 17504 | OA
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.)
 
[2]
2021 | Published | Conference Paper | IST-REx-ID: 17505 | OA
Sammler, M. J., Lepigre, R., Krebbers, R., Memarian, K., Dreyer, D., & Garg, D. (2021). RefinedC: Automating the foundational verification of C code with refined ownership types. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (pp. 158–174). virtual: Association for Computing Machinery. https://doi.org/10.1145/3453483.3454036
[Published Version] View | DOI | Download Published Version (ext.)
 
[1]
2019 | Published | Journal Article | IST-REx-ID: 17506 | OA
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.)
 
Marked Publication(s)

Search

Filter Publications

  • 16 OA Fulltext(s)

Display / Sort

Citation Style: APA

Export / Embed

Grants


17 Publications

Mark all

[17]
2026 | Published | Journal Article | IST-REx-ID: 21041 | OA | PlanS
Mück, N., Georges, A. L., Dreyer, D., Garg, D., & Sammler, M. J. (2026). Endangered by the language but saved by the compiler: Robust safety via semantic back-translation. Proceedings of the ACM on Programming Languages. Association for Computing Machinery. https://doi.org/10.1145/3776682
[Published Version] View | Files available | DOI
 
[16]
2026 | Published | Conference Paper | IST-REx-ID: 21133 | OA
Elbeheiry, L., Sammler, M. J., Krebbers, R., Dreyer, D., & Garg, D. (2026). A recipe for modular verification of generic tree traversals. In Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs (pp. 339–352). Rennes, France: Association for Computing Machinery. https://doi.org/10.1145/3779031.3779110
[Published Version] View | Files available | DOI
 
[15]
2025 | Published | Journal Article | IST-REx-ID: 21052 | OA | PlanS
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
[Published Version] View | DOI | Download Published Version (ext.)
 
[14]
2025 | Published | Journal Article | IST-REx-ID: 21053 | PlanS
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
[Published Version] View | DOI | arXiv
 
[13]
2025 | Published | Journal Article | IST-REx-ID: 19935 | OA
Spies, S., Mück, N., Zeng, H., Sammler, M. J., Lattuada, A., Müller, P., & Dreyer, D. (2025). Destabilizing Iris. Proceedings of the ACM on Programming Languages. Association for Computing Machinery. https://doi.org/10.1145/3729284
[Published Version] View | Files available | DOI
 
[12]
2025 | Published | Journal Article | IST-REx-ID: 19936 | OA
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
 
[11]
2024 | Published | Journal Article | IST-REx-ID: 17495 | OA
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.)
 
[10]
2024 | Published | Journal Article | IST-REx-ID: 17497 | OA
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.)
 
[9]
2023 | Published | Journal Article | IST-REx-ID: 17498 | OA
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.)
 
[8]
2023 | Published | Journal Article | IST-REx-ID: 17499 | OA
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.)
 
[7]
2023 | Published | Journal Article | IST-REx-ID: 17500 | OA
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.)
 
[6]
2022 | Published | Journal Article | IST-REx-ID: 17501 | OA
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.)
 
[5]
2022 | Published | Conference Paper | IST-REx-ID: 17502 | OA
Sammler, M. J., Hammond, A., Lepigre, R., Campbell, B., Pichon-Pharabod, J., Dreyer, D., … Sewell, P. (2022). Islaris: Verification of machine code against authoritative ISA semantics. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (pp. 825–840). San Diego, CA, United States: Association for Computing Machinery. https://doi.org/10.1145/3519939.3523434
[Published Version] View | DOI | Download Published Version (ext.)
 
[4]
2022 | Published | Journal Article | IST-REx-ID: 17503 | OA
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.)
 
[3]
2022 | Published | Journal Article | IST-REx-ID: 17504 | OA
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.)
 
[2]
2021 | Published | Conference Paper | IST-REx-ID: 17505 | OA
Sammler, M. J., Lepigre, R., Krebbers, R., Memarian, K., Dreyer, D., & Garg, D. (2021). RefinedC: Automating the foundational verification of C code with refined ownership types. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (pp. 158–174). virtual: Association for Computing Machinery. https://doi.org/10.1145/3453483.3454036
[Published Version] View | DOI | Download Published Version (ext.)
 
[1]
2019 | Published | Journal Article | IST-REx-ID: 17506 | OA
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.)
 
Marked Publication(s)

Search

Filter Publications

  • 16 OA Fulltext(s)

Display / Sort

Citation Style: APA

Export / Embed