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. Endangered by the language but saved by the compiler: Robust safety via semantic back-translation. Proceedings of the ACM on Programming Languages. 2026;10:1153-1182. doi:10.1145/3776682
[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. A recipe for modular verification of generic tree traversals. In: Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs. Association for Computing Machinery; 2026:339-352. doi:10.1145/3779031.3779110
[Published Version] View | Files available | DOI
 
[15]
2025 | Published | Journal Article | IST-REx-ID: 21052 | OA | PlanS
Vistrup M, Sammler MJ, Jung R. Program logics à la Carte. Proceedings of the ACM on Programming Languages. 2025;9(POPL):300-331. doi:10.1145/3704847
[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. Formal foundations for translational separation logic verifiers. Proceedings of the ACM on Programming Languages. 2025;9(POPL):569-599. doi: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, et al. Destabilizing Iris. Proceedings of the ACM on Programming Languages. 2025;9(PLDI):848-873. doi:10.1145/3729284
[Published Version] View | Files available | DOI
 
[12]
2025 | Published | Journal Article | IST-REx-ID: 19936 | OA
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
 
[11]
2024 | Published | Journal Article | IST-REx-ID: 17495 | OA
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.)
 
[10]
2024 | Published | Journal Article | IST-REx-ID: 17497 | OA
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.)
 
[9]
2023 | Published | Journal Article | IST-REx-ID: 17498 | OA
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.)
 
[8]
2023 | Published | Journal Article | IST-REx-ID: 17499 | OA
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.)
 
[7]
2023 | Published | Journal Article | IST-REx-ID: 17500 | OA
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.)
 
[6]
2022 | Published | Journal Article | IST-REx-ID: 17501 | OA
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.)
 
[5]
2022 | Published | Conference Paper | IST-REx-ID: 17502 | OA
Sammler MJ, Hammond A, Lepigre R, et al. Islaris: Verification of machine code against authoritative ISA semantics. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. Association for Computing Machinery; 2022:825-840. doi: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 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.)
 
[3]
2022 | Published | Journal Article | IST-REx-ID: 17504 | OA
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.)
 
[2]
2021 | Published | Conference Paper | IST-REx-ID: 17505 | OA
Sammler MJ, Lepigre R, Krebbers R, Memarian K, Dreyer D, Garg D. 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. Association for Computing Machinery; 2021:158-174. doi:10.1145/3453483.3454036
[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. 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.)
 
Marked Publication(s)

Search

Filter Publications

  • 16 OA Fulltext(s)

Display / Sort

Citation Style: AMA

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. Endangered by the language but saved by the compiler: Robust safety via semantic back-translation. Proceedings of the ACM on Programming Languages. 2026;10:1153-1182. doi:10.1145/3776682
[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. A recipe for modular verification of generic tree traversals. In: Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs. Association for Computing Machinery; 2026:339-352. doi:10.1145/3779031.3779110
[Published Version] View | Files available | DOI
 
[15]
2025 | Published | Journal Article | IST-REx-ID: 21052 | OA | PlanS
Vistrup M, Sammler MJ, Jung R. Program logics à la Carte. Proceedings of the ACM on Programming Languages. 2025;9(POPL):300-331. doi:10.1145/3704847
[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. Formal foundations for translational separation logic verifiers. Proceedings of the ACM on Programming Languages. 2025;9(POPL):569-599. doi: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, et al. Destabilizing Iris. Proceedings of the ACM on Programming Languages. 2025;9(PLDI):848-873. doi:10.1145/3729284
[Published Version] View | Files available | DOI
 
[12]
2025 | Published | Journal Article | IST-REx-ID: 19936 | OA
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
 
[11]
2024 | Published | Journal Article | IST-REx-ID: 17495 | OA
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.)
 
[10]
2024 | Published | Journal Article | IST-REx-ID: 17497 | OA
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.)
 
[9]
2023 | Published | Journal Article | IST-REx-ID: 17498 | OA
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.)
 
[8]
2023 | Published | Journal Article | IST-REx-ID: 17499 | OA
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.)
 
[7]
2023 | Published | Journal Article | IST-REx-ID: 17500 | OA
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.)
 
[6]
2022 | Published | Journal Article | IST-REx-ID: 17501 | OA
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.)
 
[5]
2022 | Published | Conference Paper | IST-REx-ID: 17502 | OA
Sammler MJ, Hammond A, Lepigre R, et al. Islaris: Verification of machine code against authoritative ISA semantics. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. Association for Computing Machinery; 2022:825-840. doi: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 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.)
 
[3]
2022 | Published | Journal Article | IST-REx-ID: 17504 | OA
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.)
 
[2]
2021 | Published | Conference Paper | IST-REx-ID: 17505 | OA
Sammler MJ, Lepigre R, Krebbers R, Memarian K, Dreyer D, Garg D. 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. Association for Computing Machinery; 2021:158-174. doi:10.1145/3453483.3454036
[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. 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.)
 
Marked Publication(s)

Search

Filter Publications

  • 16 OA Fulltext(s)

Display / Sort

Citation Style: AMA

Export / Embed