Michael Joachim Sammler

17 Publications

Mark all

[17]
2026 | Published | Journal Article | IST-REx-ID: 21041 | OA | PlanS
Mück, Niklas, et al. “Endangered by the Language but Saved by the Compiler: Robust Safety via Semantic Back-Translation.” Proceedings of the ACM on Programming Languages, vol. 10, Association for Computing Machinery, 2026, pp. 1153–82, doi:10.1145/3776682.
[Published Version] View | Files available | DOI
 
[16]
2026 | Published | Conference Paper | IST-REx-ID: 21133 | OA
Elbeheiry, Laila, et al. “A Recipe for Modular Verification of Generic Tree Traversals.” Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, Association for Computing Machinery, 2026, pp. 339–52, doi:10.1145/3779031.3779110.
[Published Version] View | Files available | DOI
 
[15]
2025 | Published | Journal Article | IST-REx-ID: 21052 | OA | PlanS
Vistrup, Max, et al. “Program Logics à La Carte.” Proceedings of the ACM on Programming Languages, vol. 9, no. POPL, Association for Computing Machinery, 2025, pp. 300–31, doi:10.1145/3704847.
[Published Version] View | DOI | Download Published Version (ext.)
 
[14]
2025 | Published | Journal Article | IST-REx-ID: 21053 | PlanS
Dardinier, Thibault, et al. “Formal Foundations for Translational Separation Logic Verifiers.” Proceedings of the ACM on Programming Languages, vol. 9, no. POPL, Association for Computing Machinery, 2025, pp. 569–99, doi:10.1145/3704856.
[Published Version] View | DOI | arXiv
 
[13]
2025 | Published | Journal Article | IST-REx-ID: 19935 | OA
Spies, Simon, et al. “Destabilizing Iris.” Proceedings of the ACM on Programming Languages, vol. 9, no. PLDI, Association for Computing Machinery, 2025, pp. 848–73, doi:10.1145/3729284.
[Published Version] View | Files available | DOI
 
[12]
2025 | Published | Journal Article | IST-REx-ID: 19936 | OA
Bedarkar, Kimaya, et al. “RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers.” Proceedings of the ACM on Programming Languages, vol. 9, no. PLDI, Association for Computing Machinery, 2025, pp. 73–97, doi:10.1145/3729249.
[Published Version] View | Files available | DOI
 
[11]
2024 | Published | Journal Article | IST-REx-ID: 17495 | OA
Gäher, Lennard, et al. “RefinedRust: A Type System for High-Assurance Verification of Rust Programs.” Proceedings of the ACM on Programming Languages, vol. 8, no. PLDI, Association for Computing Machinery, 2024, pp. 1115–39, doi:10.1145/3656422.
[Published Version] View | DOI | Download Published Version (ext.)
 
[10]
2024 | Published | Journal Article | IST-REx-ID: 17497 | OA
Spies, Simon, et al. “Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq.” Proceedings of the ACM on Programming Languages, vol. 8, no. PLDI, Association for Computing Machinery, 2024, pp. 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, Armaël, et al. “Melocoton: A Program Logic for Verified Interoperability between OCaml and C.” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA2, Association for Computing Machinery, 2023, pp. 716–44, doi:10.1145/3622823.
[Published Version] View | DOI | Download Published Version (ext.)
 
[8]
2023 | Published | Journal Article | IST-REx-ID: 17499 | OA
Song, Youngju, et al. “Conditional Contextual Refinement.” Proceedings of the ACM on Programming Languages, vol. 7, no. POPL, Association for Computing Machinery, 2023, pp. 1121–51, doi:10.1145/3571232.
[Published Version] View | DOI | Download Published Version (ext.)
 
[7]
2023 | Published | Journal Article | IST-REx-ID: 17500 | OA
Sammler, Michael Joachim, et al. “DimSum: A Decentralized Approach to Multi-Language Semantics and Verification.” Proceedings of the ACM on Programming Languages, vol. 7, no. POPL, Association for Computing Machinery, 2023, pp. 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, Fengmin, et al. “BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs.” Proceedings of the ACM on Programming Languages, vol. 6, no. OOPSLA2, Association for Computing Machinery, 2022, pp. 1613–38, doi:10.1145/3563345.
[Published Version] View | DOI | Download Published Version (ext.)
 
[5]
2022 | Published | Conference Paper | IST-REx-ID: 17502 | OA
Sammler, Michael Joachim, et al. “Islaris: Verification of Machine Code against Authoritative ISA Semantics.” Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2022, pp. 825–40, doi:10.1145/3519939.3523434.
[Published Version] View | DOI | Download Published Version (ext.)
 
[4]
2022 | Published | Journal Article | IST-REx-ID: 17503 | OA
Lepigre, Rodolphe, et al. “VIP: Verifying Real-World C Idioms with Integer-Pointer Casts.” Proceedings of the ACM on Programming Languages, vol. 6, no. POPL, Association for Computing Machinery, 2022, pp. 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, Lennard, et al. “Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations.” Proceedings of the ACM on Programming Languages, vol. 6, no. POPL, Association for Computing Machinery, 2022, pp. 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, Michael Joachim, et al. “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, Association for Computing Machinery, 2021, pp. 158–74, doi: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, et al. “The High-Level Benefits of Low-Level Sandboxing.” Proceedings of the ACM on Programming Languages, vol. 4, no. POPL, Association for Computing Machinery, 2019, pp. 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: MLA

Export / Embed

Grants


17 Publications

Mark all

[17]
2026 | Published | Journal Article | IST-REx-ID: 21041 | OA | PlanS
Mück, Niklas, et al. “Endangered by the Language but Saved by the Compiler: Robust Safety via Semantic Back-Translation.” Proceedings of the ACM on Programming Languages, vol. 10, Association for Computing Machinery, 2026, pp. 1153–82, doi:10.1145/3776682.
[Published Version] View | Files available | DOI
 
[16]
2026 | Published | Conference Paper | IST-REx-ID: 21133 | OA
Elbeheiry, Laila, et al. “A Recipe for Modular Verification of Generic Tree Traversals.” Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, Association for Computing Machinery, 2026, pp. 339–52, doi:10.1145/3779031.3779110.
[Published Version] View | Files available | DOI
 
[15]
2025 | Published | Journal Article | IST-REx-ID: 21052 | OA | PlanS
Vistrup, Max, et al. “Program Logics à La Carte.” Proceedings of the ACM on Programming Languages, vol. 9, no. POPL, Association for Computing Machinery, 2025, pp. 300–31, doi:10.1145/3704847.
[Published Version] View | DOI | Download Published Version (ext.)
 
[14]
2025 | Published | Journal Article | IST-REx-ID: 21053 | PlanS
Dardinier, Thibault, et al. “Formal Foundations for Translational Separation Logic Verifiers.” Proceedings of the ACM on Programming Languages, vol. 9, no. POPL, Association for Computing Machinery, 2025, pp. 569–99, doi:10.1145/3704856.
[Published Version] View | DOI | arXiv
 
[13]
2025 | Published | Journal Article | IST-REx-ID: 19935 | OA
Spies, Simon, et al. “Destabilizing Iris.” Proceedings of the ACM on Programming Languages, vol. 9, no. PLDI, Association for Computing Machinery, 2025, pp. 848–73, doi:10.1145/3729284.
[Published Version] View | Files available | DOI
 
[12]
2025 | Published | Journal Article | IST-REx-ID: 19936 | OA
Bedarkar, Kimaya, et al. “RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers.” Proceedings of the ACM on Programming Languages, vol. 9, no. PLDI, Association for Computing Machinery, 2025, pp. 73–97, doi:10.1145/3729249.
[Published Version] View | Files available | DOI
 
[11]
2024 | Published | Journal Article | IST-REx-ID: 17495 | OA
Gäher, Lennard, et al. “RefinedRust: A Type System for High-Assurance Verification of Rust Programs.” Proceedings of the ACM on Programming Languages, vol. 8, no. PLDI, Association for Computing Machinery, 2024, pp. 1115–39, doi:10.1145/3656422.
[Published Version] View | DOI | Download Published Version (ext.)
 
[10]
2024 | Published | Journal Article | IST-REx-ID: 17497 | OA
Spies, Simon, et al. “Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq.” Proceedings of the ACM on Programming Languages, vol. 8, no. PLDI, Association for Computing Machinery, 2024, pp. 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, Armaël, et al. “Melocoton: A Program Logic for Verified Interoperability between OCaml and C.” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA2, Association for Computing Machinery, 2023, pp. 716–44, doi:10.1145/3622823.
[Published Version] View | DOI | Download Published Version (ext.)
 
[8]
2023 | Published | Journal Article | IST-REx-ID: 17499 | OA
Song, Youngju, et al. “Conditional Contextual Refinement.” Proceedings of the ACM on Programming Languages, vol. 7, no. POPL, Association for Computing Machinery, 2023, pp. 1121–51, doi:10.1145/3571232.
[Published Version] View | DOI | Download Published Version (ext.)
 
[7]
2023 | Published | Journal Article | IST-REx-ID: 17500 | OA
Sammler, Michael Joachim, et al. “DimSum: A Decentralized Approach to Multi-Language Semantics and Verification.” Proceedings of the ACM on Programming Languages, vol. 7, no. POPL, Association for Computing Machinery, 2023, pp. 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, Fengmin, et al. “BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs.” Proceedings of the ACM on Programming Languages, vol. 6, no. OOPSLA2, Association for Computing Machinery, 2022, pp. 1613–38, doi:10.1145/3563345.
[Published Version] View | DOI | Download Published Version (ext.)
 
[5]
2022 | Published | Conference Paper | IST-REx-ID: 17502 | OA
Sammler, Michael Joachim, et al. “Islaris: Verification of Machine Code against Authoritative ISA Semantics.” Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2022, pp. 825–40, doi:10.1145/3519939.3523434.
[Published Version] View | DOI | Download Published Version (ext.)
 
[4]
2022 | Published | Journal Article | IST-REx-ID: 17503 | OA
Lepigre, Rodolphe, et al. “VIP: Verifying Real-World C Idioms with Integer-Pointer Casts.” Proceedings of the ACM on Programming Languages, vol. 6, no. POPL, Association for Computing Machinery, 2022, pp. 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, Lennard, et al. “Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations.” Proceedings of the ACM on Programming Languages, vol. 6, no. POPL, Association for Computing Machinery, 2022, pp. 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, Michael Joachim, et al. “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, Association for Computing Machinery, 2021, pp. 158–74, doi: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, et al. “The High-Level Benefits of Low-Level Sandboxing.” Proceedings of the ACM on Programming Languages, vol. 4, no. POPL, Association for Computing Machinery, 2019, pp. 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: MLA

Export / Embed