Michael Joachim Sammler

17 Publications

Mark all

[17]
2026 | Published | Journal Article | IST-REx-ID: 21041 | OA | PlanS
Mück, Niklas, Aïna Linn Georges, Derek Dreyer, Deepak Garg, and Michael Joachim Sammler. “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, 2026. https://doi.org/10.1145/3776682.
[Published Version] View | Files available | DOI
 
[16]
2026 | Published | Conference Paper | IST-REx-ID: 21133 | OA
Elbeheiry, Laila, Michael Joachim Sammler, Robbert Krebbers, Derek Dreyer, and Deepak Garg. “A Recipe for Modular Verification of Generic Tree Traversals.” In Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, 339–52. Association for Computing Machinery, 2026. 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, Max, Michael Joachim Sammler, and Ralf Jung. “Program Logics à La Carte.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2025. 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, Thibault, Michael Joachim Sammler, Gaurav Parthasarathy, Alexander J. Summers, and Peter Müller. “Formal Foundations for Translational Separation Logic Verifiers.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2025. https://doi.org/10.1145/3704856.
[Published Version] View | DOI | arXiv
 
[13]
2025 | Published | Journal Article | IST-REx-ID: 19935 | OA
Spies, Simon, Niklas Mück, Haoyi Zeng, Michael Joachim Sammler, Andrea Lattuada, Peter Müller, and Derek Dreyer. “Destabilizing Iris.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2025. https://doi.org/10.1145/3729284.
[Published Version] View | Files available | DOI
 
[12]
2025 | Published | Journal Article | IST-REx-ID: 19936 | OA
Bedarkar, Kimaya, Laila Elbeheiry, Michael Joachim Sammler, Lennard Gäher, Björn Brandenburg, Derek Dreyer, and Deepak Garg. “RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2025. https://doi.org/10.1145/3729249.
[Published Version] View | Files available | DOI
 
[11]
2024 | Published | Journal Article | IST-REx-ID: 17495 | OA
Gäher, Lennard, Michael Joachim Sammler, Ralf Jung, Robbert Krebbers, and Derek Dreyer. “RefinedRust: A Type System for High-Assurance Verification of Rust Programs.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2024. 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, Simon, Lennard Gäher, Michael Joachim Sammler, and Derek Dreyer. “Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2024. 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, Armaël, Johannes Hostert, Simon Spies, Michael Joachim Sammler, Lars Birkedal, and Derek Dreyer. “Melocoton: A Program Logic for Verified Interoperability between OCaml and C.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2023. 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, Youngju, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Joachim Sammler, and Derek Dreyer. “Conditional Contextual Refinement.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2023. 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, Michael Joachim, Simon Spies, Youngju Song, Emanuele D’Osualdo, Robbert Krebbers, Deepak Garg, and Derek Dreyer. “DimSum: A Decentralized Approach to Multi-Language Semantics and Verification.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2023. 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, Fengmin, Michael Joachim Sammler, Rodolphe Lepigre, Derek Dreyer, and Deepak Garg. “BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2022. 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, Michael Joachim, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, and Peter Sewell. “Islaris: Verification of Machine Code against Authoritative ISA Semantics.” In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 825–40. Association for Computing Machinery, 2022. 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, Rodolphe, Michael Joachim Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, and Peter Sewell. “VIP: Verifying Real-World C Idioms with Integer-Pointer Casts.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2022. 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, Lennard, Michael Joachim Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer. “Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2022. 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, Michael Joachim, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, and Deepak Garg. “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, 158–74. Association for Computing Machinery, 2021. 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, Michael Joachim, Deepak Garg, Derek Dreyer, and Tadeusz Litak. “The High-Level Benefits of Low-Level Sandboxing.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2019. 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: Chicago

Export / Embed

Grants


17 Publications

Mark all

[17]
2026 | Published | Journal Article | IST-REx-ID: 21041 | OA | PlanS
Mück, Niklas, Aïna Linn Georges, Derek Dreyer, Deepak Garg, and Michael Joachim Sammler. “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, 2026. https://doi.org/10.1145/3776682.
[Published Version] View | Files available | DOI
 
[16]
2026 | Published | Conference Paper | IST-REx-ID: 21133 | OA
Elbeheiry, Laila, Michael Joachim Sammler, Robbert Krebbers, Derek Dreyer, and Deepak Garg. “A Recipe for Modular Verification of Generic Tree Traversals.” In Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, 339–52. Association for Computing Machinery, 2026. 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, Max, Michael Joachim Sammler, and Ralf Jung. “Program Logics à La Carte.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2025. 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, Thibault, Michael Joachim Sammler, Gaurav Parthasarathy, Alexander J. Summers, and Peter Müller. “Formal Foundations for Translational Separation Logic Verifiers.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2025. https://doi.org/10.1145/3704856.
[Published Version] View | DOI | arXiv
 
[13]
2025 | Published | Journal Article | IST-REx-ID: 19935 | OA
Spies, Simon, Niklas Mück, Haoyi Zeng, Michael Joachim Sammler, Andrea Lattuada, Peter Müller, and Derek Dreyer. “Destabilizing Iris.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2025. https://doi.org/10.1145/3729284.
[Published Version] View | Files available | DOI
 
[12]
2025 | Published | Journal Article | IST-REx-ID: 19936 | OA
Bedarkar, Kimaya, Laila Elbeheiry, Michael Joachim Sammler, Lennard Gäher, Björn Brandenburg, Derek Dreyer, and Deepak Garg. “RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2025. https://doi.org/10.1145/3729249.
[Published Version] View | Files available | DOI
 
[11]
2024 | Published | Journal Article | IST-REx-ID: 17495 | OA
Gäher, Lennard, Michael Joachim Sammler, Ralf Jung, Robbert Krebbers, and Derek Dreyer. “RefinedRust: A Type System for High-Assurance Verification of Rust Programs.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2024. 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, Simon, Lennard Gäher, Michael Joachim Sammler, and Derek Dreyer. “Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2024. 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, Armaël, Johannes Hostert, Simon Spies, Michael Joachim Sammler, Lars Birkedal, and Derek Dreyer. “Melocoton: A Program Logic for Verified Interoperability between OCaml and C.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2023. 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, Youngju, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Joachim Sammler, and Derek Dreyer. “Conditional Contextual Refinement.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2023. 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, Michael Joachim, Simon Spies, Youngju Song, Emanuele D’Osualdo, Robbert Krebbers, Deepak Garg, and Derek Dreyer. “DimSum: A Decentralized Approach to Multi-Language Semantics and Verification.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2023. 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, Fengmin, Michael Joachim Sammler, Rodolphe Lepigre, Derek Dreyer, and Deepak Garg. “BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2022. 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, Michael Joachim, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, and Peter Sewell. “Islaris: Verification of Machine Code against Authoritative ISA Semantics.” In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 825–40. Association for Computing Machinery, 2022. 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, Rodolphe, Michael Joachim Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, and Peter Sewell. “VIP: Verifying Real-World C Idioms with Integer-Pointer Casts.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2022. 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, Lennard, Michael Joachim Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer. “Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2022. 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, Michael Joachim, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, and Deepak Garg. “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, 158–74. Association for Computing Machinery, 2021. 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, Michael Joachim, Deepak Garg, Derek Dreyer, and Tadeusz Litak. “The High-Level Benefits of Low-Level Sandboxing.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2019. 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: Chicago

Export / Embed