Michael Joachim Sammler

13 Publications

Mark all

[13]
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
 
[12]
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
 
[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

Display / Sort

Citation Style: Chicago

Export / Embed

Grants


13 Publications

Mark all

[13]
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
 
[12]
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
 
[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

Display / Sort

Citation Style: Chicago

Export / Embed