Michael Joachim Sammler

13 Publications

Mark all

[13]
2025 | Published | Journal Article | IST-REx-ID: 19936 | OA
Bedarkar K, Elbeheiry L, Sammler MJ, Gäher L, Brandenburg B, Dreyer D, Garg D. 2025. RefinedProsa: Connecting response-time analysis with C verification for interrupt-free schedulers. Proceedings of the ACM on Programming Languages. 9(PLDI), 73–97.
[Published Version] View | Files available | DOI
 
[12]
2025 | Published | Journal Article | IST-REx-ID: 19935 | OA
Spies S, Mück N, Zeng H, Sammler MJ, Lattuada A, Müller P, Dreyer D. 2025. Destabilizing Iris. Proceedings of the ACM on Programming Languages. 9(PLDI), 848–873.
[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. 2024. RefinedRust: A type system for high-assurance verification of rust programs. Proceedings of the ACM on Programming Languages. 8(PLDI), 1115–1139.
[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. 2024. Quiver: Guided abductive inference of separation logic specifications in coq. Proceedings of the ACM on Programming Languages. 8(PLDI), 889–913.
[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. 2023. Melocoton: A program logic for verified interoperability between OCaml and C. Proceedings of the ACM on Programming Languages. 7(OOPSLA2), 716–744.
[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. 2023. Conditional contextual refinement. Proceedings of the ACM on Programming Languages. 7(POPL), 1121–1151.
[Published Version] View | DOI | Download Published Version (ext.)
 
[7]
2023 | Published | Journal Article | IST-REx-ID: 17500 | OA
Sammler MJ, Spies S, Song Y, D’Osualdo E, Krebbers R, Garg D, Dreyer D. 2023. DimSum: A decentralized approach to multi-language semantics and verification. Proceedings of the ACM on Programming Languages. 7(POPL), 775–805.
[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. 2022. BFF: Foundational and automated verification of bitfield-manipulating programs. Proceedings of the ACM on Programming Languages. 6(OOPSLA2), 1613–1638.
[Published Version] View | DOI | Download Published Version (ext.)
 
[5]
2022 | Published | Conference Paper | IST-REx-ID: 17502 | OA
Sammler MJ, Hammond A, Lepigre R, Campbell B, Pichon-Pharabod J, Dreyer D, Garg D, Sewell P. 2022. Islaris: Verification of machine code against authoritative ISA semantics. Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Conference on Programming Language Design and Implementation, 825–840.
[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. 2022. VIP: Verifying real-world C idioms with integer-pointer casts. Proceedings of the ACM on Programming Languages. 6(POPL), 1–32.
[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, Jung R, Dang H-H, Krebbers R, Kang J, Dreyer D. 2022. Simuliris: A separation logic framework for verifying concurrent program optimizations. Proceedings of the ACM on Programming Languages. 6(POPL), 1–31.
[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. 2021. 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. PLDI: Conference on Programming Language Design and Implementation, 158–174.
[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. 2019. The high-level benefits of low-level sandboxing. Proceedings of the ACM on Programming Languages. 4(POPL), 1–32.
[Published Version] View | DOI | Download Published Version (ext.)
 
Marked Publication(s)

Search

Filter Publications

Display / Sort

Citation Style: ISTA Annual Report

Export / Embed

Grants


13 Publications

Mark all

[13]
2025 | Published | Journal Article | IST-REx-ID: 19936 | OA
Bedarkar K, Elbeheiry L, Sammler MJ, Gäher L, Brandenburg B, Dreyer D, Garg D. 2025. RefinedProsa: Connecting response-time analysis with C verification for interrupt-free schedulers. Proceedings of the ACM on Programming Languages. 9(PLDI), 73–97.
[Published Version] View | Files available | DOI
 
[12]
2025 | Published | Journal Article | IST-REx-ID: 19935 | OA
Spies S, Mück N, Zeng H, Sammler MJ, Lattuada A, Müller P, Dreyer D. 2025. Destabilizing Iris. Proceedings of the ACM on Programming Languages. 9(PLDI), 848–873.
[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. 2024. RefinedRust: A type system for high-assurance verification of rust programs. Proceedings of the ACM on Programming Languages. 8(PLDI), 1115–1139.
[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. 2024. Quiver: Guided abductive inference of separation logic specifications in coq. Proceedings of the ACM on Programming Languages. 8(PLDI), 889–913.
[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. 2023. Melocoton: A program logic for verified interoperability between OCaml and C. Proceedings of the ACM on Programming Languages. 7(OOPSLA2), 716–744.
[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. 2023. Conditional contextual refinement. Proceedings of the ACM on Programming Languages. 7(POPL), 1121–1151.
[Published Version] View | DOI | Download Published Version (ext.)
 
[7]
2023 | Published | Journal Article | IST-REx-ID: 17500 | OA
Sammler MJ, Spies S, Song Y, D’Osualdo E, Krebbers R, Garg D, Dreyer D. 2023. DimSum: A decentralized approach to multi-language semantics and verification. Proceedings of the ACM on Programming Languages. 7(POPL), 775–805.
[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. 2022. BFF: Foundational and automated verification of bitfield-manipulating programs. Proceedings of the ACM on Programming Languages. 6(OOPSLA2), 1613–1638.
[Published Version] View | DOI | Download Published Version (ext.)
 
[5]
2022 | Published | Conference Paper | IST-REx-ID: 17502 | OA
Sammler MJ, Hammond A, Lepigre R, Campbell B, Pichon-Pharabod J, Dreyer D, Garg D, Sewell P. 2022. Islaris: Verification of machine code against authoritative ISA semantics. Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Conference on Programming Language Design and Implementation, 825–840.
[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. 2022. VIP: Verifying real-world C idioms with integer-pointer casts. Proceedings of the ACM on Programming Languages. 6(POPL), 1–32.
[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, Jung R, Dang H-H, Krebbers R, Kang J, Dreyer D. 2022. Simuliris: A separation logic framework for verifying concurrent program optimizations. Proceedings of the ACM on Programming Languages. 6(POPL), 1–31.
[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. 2021. 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. PLDI: Conference on Programming Language Design and Implementation, 158–174.
[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. 2019. The high-level benefits of low-level sandboxing. Proceedings of the ACM on Programming Languages. 4(POPL), 1–32.
[Published Version] View | DOI | Download Published Version (ext.)
 
Marked Publication(s)

Search

Filter Publications

Display / Sort

Citation Style: ISTA Annual Report

Export / Embed