Michael Joachim Sammler

13 Publications

Mark all

[13]
2025 | Published | Journal Article | IST-REx-ID: 19936 | OA
K. Bedarkar 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, pp. 73–97, 2025.
[Published Version] View | Files available | DOI
 
[12]
2025 | Published | Journal Article | IST-REx-ID: 19935 | OA
S. Spies et al., “Destabilizing Iris,” Proceedings of the ACM on Programming Languages, vol. 9, no. PLDI. Association for Computing Machinery, pp. 848–873, 2025.
[Published Version] View | Files available | DOI
 
[11]
2024 | Published | Journal Article | IST-REx-ID: 17495 | OA
L. Gäher, M. J. Sammler, R. Jung, R. Krebbers, and D. Dreyer, “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, pp. 1115–1139, 2024.
[Published Version] View | DOI | Download Published Version (ext.)
 
[10]
2024 | Published | Journal Article | IST-REx-ID: 17497 | OA
S. Spies, L. Gäher, M. J. Sammler, and D. Dreyer, “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, pp. 889–913, 2024.
[Published Version] View | DOI | Download Published Version (ext.)
 
[9]
2023 | Published | Journal Article | IST-REx-ID: 17498 | OA
A. Guéneau, J. Hostert, S. Spies, M. J. Sammler, L. Birkedal, and D. Dreyer, “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, pp. 716–744, 2023.
[Published Version] View | DOI | Download Published Version (ext.)
 
[8]
2023 | Published | Journal Article | IST-REx-ID: 17499 | OA
Y. Song, M. Cho, D. Lee, C.-K. Hur, M. J. Sammler, and D. Dreyer, “Conditional contextual refinement,” Proceedings of the ACM on Programming Languages, vol. 7, no. POPL. Association for Computing Machinery, pp. 1121–1151, 2023.
[Published Version] View | DOI | Download Published Version (ext.)
 
[7]
2023 | Published | Journal Article | IST-REx-ID: 17500 | OA
M. J. Sammler 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, pp. 775–805, 2023.
[Published Version] View | DOI | Download Published Version (ext.)
 
[6]
2022 | Published | Journal Article | IST-REx-ID: 17501 | OA
F. Zhu, M. J. Sammler, R. Lepigre, D. Dreyer, and D. Garg, “BFF: Foundational and automated verification of bitfield-manipulating programs,” Proceedings of the ACM on Programming Languages, vol. 6, no. OOPSLA2. Association for Computing Machinery, pp. 1613–1638, 2022.
[Published Version] View | DOI | Download Published Version (ext.)
 
[5]
2022 | Published | Conference Paper | IST-REx-ID: 17502 | OA
M. J. Sammler et al., “Islaris: Verification of machine code against authoritative ISA semantics,” in Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, United States, 2022, pp. 825–840.
[Published Version] View | DOI | Download Published Version (ext.)
 
[4]
2022 | Published | Journal Article | IST-REx-ID: 17503 | OA
R. Lepigre, M. J. Sammler, K. Memarian, R. Krebbers, D. Dreyer, and P. Sewell, “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, pp. 1–32, 2022.
[Published Version] View | DOI | Download Published Version (ext.)
 
[3]
2022 | Published | Journal Article | IST-REx-ID: 17504 | OA
L. Gäher 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, pp. 1–31, 2022.
[Published Version] View | DOI | Download Published Version (ext.)
 
[2]
2021 | Published | Conference Paper | IST-REx-ID: 17505 | OA
M. J. Sammler, R. Lepigre, R. Krebbers, K. Memarian, D. Dreyer, and D. 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, virtual, 2021, pp. 158–174.
[Published Version] View | DOI | Download Published Version (ext.)
 
[1]
2019 | Published | Journal Article | IST-REx-ID: 17506 | OA
M. J. Sammler, D. Garg, D. Dreyer, and T. Litak, “The high-level benefits of low-level sandboxing,” Proceedings of the ACM on Programming Languages, vol. 4, no. POPL. Association for Computing Machinery, pp. 1–32, 2019.
[Published Version] View | DOI | Download Published Version (ext.)
 
Marked Publication(s)

Search

Filter Publications

Display / Sort

Citation Style: IEEE

Export / Embed

Grants


13 Publications

Mark all

[13]
2025 | Published | Journal Article | IST-REx-ID: 19936 | OA
K. Bedarkar 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, pp. 73–97, 2025.
[Published Version] View | Files available | DOI
 
[12]
2025 | Published | Journal Article | IST-REx-ID: 19935 | OA
S. Spies et al., “Destabilizing Iris,” Proceedings of the ACM on Programming Languages, vol. 9, no. PLDI. Association for Computing Machinery, pp. 848–873, 2025.
[Published Version] View | Files available | DOI
 
[11]
2024 | Published | Journal Article | IST-REx-ID: 17495 | OA
L. Gäher, M. J. Sammler, R. Jung, R. Krebbers, and D. Dreyer, “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, pp. 1115–1139, 2024.
[Published Version] View | DOI | Download Published Version (ext.)
 
[10]
2024 | Published | Journal Article | IST-REx-ID: 17497 | OA
S. Spies, L. Gäher, M. J. Sammler, and D. Dreyer, “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, pp. 889–913, 2024.
[Published Version] View | DOI | Download Published Version (ext.)
 
[9]
2023 | Published | Journal Article | IST-REx-ID: 17498 | OA
A. Guéneau, J. Hostert, S. Spies, M. J. Sammler, L. Birkedal, and D. Dreyer, “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, pp. 716–744, 2023.
[Published Version] View | DOI | Download Published Version (ext.)
 
[8]
2023 | Published | Journal Article | IST-REx-ID: 17499 | OA
Y. Song, M. Cho, D. Lee, C.-K. Hur, M. J. Sammler, and D. Dreyer, “Conditional contextual refinement,” Proceedings of the ACM on Programming Languages, vol. 7, no. POPL. Association for Computing Machinery, pp. 1121–1151, 2023.
[Published Version] View | DOI | Download Published Version (ext.)
 
[7]
2023 | Published | Journal Article | IST-REx-ID: 17500 | OA
M. J. Sammler 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, pp. 775–805, 2023.
[Published Version] View | DOI | Download Published Version (ext.)
 
[6]
2022 | Published | Journal Article | IST-REx-ID: 17501 | OA
F. Zhu, M. J. Sammler, R. Lepigre, D. Dreyer, and D. Garg, “BFF: Foundational and automated verification of bitfield-manipulating programs,” Proceedings of the ACM on Programming Languages, vol. 6, no. OOPSLA2. Association for Computing Machinery, pp. 1613–1638, 2022.
[Published Version] View | DOI | Download Published Version (ext.)
 
[5]
2022 | Published | Conference Paper | IST-REx-ID: 17502 | OA
M. J. Sammler et al., “Islaris: Verification of machine code against authoritative ISA semantics,” in Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, United States, 2022, pp. 825–840.
[Published Version] View | DOI | Download Published Version (ext.)
 
[4]
2022 | Published | Journal Article | IST-REx-ID: 17503 | OA
R. Lepigre, M. J. Sammler, K. Memarian, R. Krebbers, D. Dreyer, and P. Sewell, “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, pp. 1–32, 2022.
[Published Version] View | DOI | Download Published Version (ext.)
 
[3]
2022 | Published | Journal Article | IST-REx-ID: 17504 | OA
L. Gäher 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, pp. 1–31, 2022.
[Published Version] View | DOI | Download Published Version (ext.)
 
[2]
2021 | Published | Conference Paper | IST-REx-ID: 17505 | OA
M. J. Sammler, R. Lepigre, R. Krebbers, K. Memarian, D. Dreyer, and D. 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, virtual, 2021, pp. 158–174.
[Published Version] View | DOI | Download Published Version (ext.)
 
[1]
2019 | Published | Journal Article | IST-REx-ID: 17506 | OA
M. J. Sammler, D. Garg, D. Dreyer, and T. Litak, “The high-level benefits of low-level sandboxing,” Proceedings of the ACM on Programming Languages, vol. 4, no. POPL. Association for Computing Machinery, pp. 1–32, 2019.
[Published Version] View | DOI | Download Published Version (ext.)
 
Marked Publication(s)

Search

Filter Publications

Display / Sort

Citation Style: IEEE

Export / Embed