Michael Joachim Sammler

17 Publications

Mark all

[17]
2026 | Published | Journal Article | IST-REx-ID: 21041 | OA | PlanS
Mück N, Georges AL, Dreyer D, Garg D, Sammler MJ. 2026. Endangered by the language but saved by the compiler: Robust safety via semantic back-translation. Proceedings of the ACM on Programming Languages. 10, 1153–1182.
[Published Version] View | Files available | DOI
 
[16]
2026 | Published | Conference Paper | IST-REx-ID: 21133 | OA
Elbeheiry L, Sammler MJ, Krebbers R, Dreyer D, Garg D. 2026. A recipe for modular verification of generic tree traversals. Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP: Conference on Certified Programs and Proofs, 339–352.
[Published Version] View | Files available | DOI
 
[15]
2025 | Published | Journal Article | IST-REx-ID: 21052 | OA | PlanS
Vistrup M, Sammler MJ, Jung R. 2025. Program logics à la Carte. Proceedings of the ACM on Programming Languages. 9(POPL), 300–331.
[Published Version] View | DOI | Download Published Version (ext.)
 
[14]
2025 | Published | Journal Article | IST-REx-ID: 21053 | PlanS
Dardinier T, Sammler MJ, Parthasarathy G, Summers AJ, Müller P. 2025. Formal foundations for translational separation logic verifiers. Proceedings of the ACM on Programming Languages. 9(POPL), 569–599.
[Published Version] View | DOI | arXiv
 
[13]
2025 | Published | Journal Article | IST-REx-ID: 19935 | OA
Spies S, Mück N, Zeng H, Sammler MJ, Lattuada A, Müller P, Dreyer D. 2025. Destabilizing Iris. Proceedings of the ACM on Programming Languages. 9(PLDI), 848–873.
[Published Version] View | Files available | DOI
 
[12]
2025 | Published | Journal Article | IST-REx-ID: 19936 | OA
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
 
[11]
2024 | Published | Journal Article | IST-REx-ID: 17495 | OA
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.)
 
[10]
2024 | Published | Journal Article | IST-REx-ID: 17497 | OA
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.)
 
[9]
2023 | Published | Journal Article | IST-REx-ID: 17498 | OA
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.)
 
[8]
2023 | Published | Journal Article | IST-REx-ID: 17499 | OA
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.)
 
[7]
2023 | Published | Journal Article | IST-REx-ID: 17500 | OA
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.)
 
[6]
2022 | Published | Journal Article | IST-REx-ID: 17501 | OA
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.)
 
[5]
2022 | Published | Conference Paper | IST-REx-ID: 17502 | OA
Sammler MJ, Hammond A, Lepigre R, Campbell B, Pichon-Pharabod J, Dreyer D, Garg D, Sewell P. 2022. Islaris: Verification of machine code against authoritative ISA semantics. Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Conference on Programming Language Design and Implementation, 825–840.
[Published Version] View | DOI | Download Published Version (ext.)
 
[4]
2022 | Published | Journal Article | IST-REx-ID: 17503 | OA
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.)
 
[3]
2022 | Published | Journal Article | IST-REx-ID: 17504 | OA
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.)
 
[2]
2021 | Published | Conference Paper | IST-REx-ID: 17505 | OA
Sammler MJ, Lepigre R, Krebbers R, Memarian K, Dreyer D, Garg D. 2021. RefinedC: Automating the foundational verification of C code with refined ownership types. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Conference on Programming Language Design and Implementation, 158–174.
[Published Version] View | DOI | Download Published Version (ext.)
 
[1]
2019 | Published | Journal Article | IST-REx-ID: 17506 | OA
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.)
 
Marked Publication(s)

Search

Filter Publications

  • 16 OA Fulltext(s)

Display / Sort

Citation Style: ISTA Annual Report

Export / Embed

Grants


17 Publications

Mark all

[17]
2026 | Published | Journal Article | IST-REx-ID: 21041 | OA | PlanS
Mück N, Georges AL, Dreyer D, Garg D, Sammler MJ. 2026. Endangered by the language but saved by the compiler: Robust safety via semantic back-translation. Proceedings of the ACM on Programming Languages. 10, 1153–1182.
[Published Version] View | Files available | DOI
 
[16]
2026 | Published | Conference Paper | IST-REx-ID: 21133 | OA
Elbeheiry L, Sammler MJ, Krebbers R, Dreyer D, Garg D. 2026. A recipe for modular verification of generic tree traversals. Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP: Conference on Certified Programs and Proofs, 339–352.
[Published Version] View | Files available | DOI
 
[15]
2025 | Published | Journal Article | IST-REx-ID: 21052 | OA | PlanS
Vistrup M, Sammler MJ, Jung R. 2025. Program logics à la Carte. Proceedings of the ACM on Programming Languages. 9(POPL), 300–331.
[Published Version] View | DOI | Download Published Version (ext.)
 
[14]
2025 | Published | Journal Article | IST-REx-ID: 21053 | PlanS
Dardinier T, Sammler MJ, Parthasarathy G, Summers AJ, Müller P. 2025. Formal foundations for translational separation logic verifiers. Proceedings of the ACM on Programming Languages. 9(POPL), 569–599.
[Published Version] View | DOI | arXiv
 
[13]
2025 | Published | Journal Article | IST-REx-ID: 19935 | OA
Spies S, Mück N, Zeng H, Sammler MJ, Lattuada A, Müller P, Dreyer D. 2025. Destabilizing Iris. Proceedings of the ACM on Programming Languages. 9(PLDI), 848–873.
[Published Version] View | Files available | DOI
 
[12]
2025 | Published | Journal Article | IST-REx-ID: 19936 | OA
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
 
[11]
2024 | Published | Journal Article | IST-REx-ID: 17495 | OA
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.)
 
[10]
2024 | Published | Journal Article | IST-REx-ID: 17497 | OA
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.)
 
[9]
2023 | Published | Journal Article | IST-REx-ID: 17498 | OA
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.)
 
[8]
2023 | Published | Journal Article | IST-REx-ID: 17499 | OA
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.)
 
[7]
2023 | Published | Journal Article | IST-REx-ID: 17500 | OA
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.)
 
[6]
2022 | Published | Journal Article | IST-REx-ID: 17501 | OA
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.)
 
[5]
2022 | Published | Conference Paper | IST-REx-ID: 17502 | OA
Sammler MJ, Hammond A, Lepigre R, Campbell B, Pichon-Pharabod J, Dreyer D, Garg D, Sewell P. 2022. Islaris: Verification of machine code against authoritative ISA semantics. Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Conference on Programming Language Design and Implementation, 825–840.
[Published Version] View | DOI | Download Published Version (ext.)
 
[4]
2022 | Published | Journal Article | IST-REx-ID: 17503 | OA
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.)
 
[3]
2022 | Published | Journal Article | IST-REx-ID: 17504 | OA
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.)
 
[2]
2021 | Published | Conference Paper | IST-REx-ID: 17505 | OA
Sammler MJ, Lepigre R, Krebbers R, Memarian K, Dreyer D, Garg D. 2021. RefinedC: Automating the foundational verification of C code with refined ownership types. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Conference on Programming Language Design and Implementation, 158–174.
[Published Version] View | DOI | Download Published Version (ext.)
 
[1]
2019 | Published | Journal Article | IST-REx-ID: 17506 | OA
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.)
 
Marked Publication(s)

Search

Filter Publications

  • 16 OA Fulltext(s)

Display / Sort

Citation Style: ISTA Annual Report

Export / Embed