Michael Joachim Sammler

13 Publications

Mark all

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

Display / Sort

Citation Style: MLA

Export / Embed

Grants


13 Publications

Mark all

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

Display / Sort

Citation Style: MLA

Export / Embed