Michael Joachim Sammler

Sammler Group

11 Publications

Mark all

[11]
2024 | Published | Journal Article | IST-REx-ID: 17495 | OA
RefinedRust: A type system for high-assurance verification of rust programs
L. Gäher, M.J. Sammler, R. Jung, R. Krebbers, D. Dreyer, Proceedings of the ACM on Programming Languages 8 (2024) 1115–1139.
[Published Version] View | DOI | Download Published Version (ext.)
 
[10]
2024 | Published | Journal Article | IST-REx-ID: 17497 | OA
Quiver: Guided abductive inference of separation logic specifications in coq
S. Spies, L. Gäher, M.J. Sammler, D. Dreyer, Proceedings of the ACM on Programming Languages 8 (2024) 889–913.
[Published Version] View | DOI | Download Published Version (ext.)
 
[9]
2023 | Published | Journal Article | IST-REx-ID: 17498 | OA
Melocoton: A program logic for verified interoperability between OCaml and C
A. Guéneau, J. Hostert, S. Spies, M.J. Sammler, L. Birkedal, D. Dreyer, Proceedings of the ACM on Programming Languages 7 (2023) 716–744.
[Published Version] View | DOI | Download Published Version (ext.)
 
[8]
2023 | Published | Journal Article | IST-REx-ID: 17499 | OA
Conditional contextual refinement
Y. Song, M. Cho, D. Lee, C.-K. Hur, M.J. Sammler, D. Dreyer, Proceedings of the ACM on Programming Languages 7 (2023) 1121–1151.
[Published Version] View | DOI | Download Published Version (ext.)
 
[7]
2023 | Published | Journal Article | IST-REx-ID: 17500 | OA
DimSum: A decentralized approach to multi-language semantics and verification
M.J. Sammler, S. Spies, Y. Song, E. D’Osualdo, R. Krebbers, D. Garg, D. Dreyer, Proceedings of the ACM on Programming Languages 7 (2023) 775–805.
[Published Version] View | DOI | Download Published Version (ext.)
 
[6]
2022 | Published | Journal Article | IST-REx-ID: 17501 | OA
BFF: Foundational and automated verification of bitfield-manipulating programs
F. Zhu, M.J. Sammler, R. Lepigre, D. Dreyer, D. Garg, Proceedings of the ACM on Programming Languages 6 (2022) 1613–1638.
[Published Version] View | DOI | Download Published Version (ext.)
 
[5]
2022 | Published | Conference Paper | IST-REx-ID: 17502 | OA
Islaris: Verification of machine code against authoritative ISA semantics
M.J. Sammler, A. Hammond, R. Lepigre, B. Campbell, J. Pichon-Pharabod, D. Dreyer, D. Garg, P. Sewell, in:, Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2022, pp. 825–840.
[Published Version] View | DOI | Download Published Version (ext.)
 
[4]
2022 | Published | Journal Article | IST-REx-ID: 17503 | OA
VIP: Verifying real-world C idioms with integer-pointer casts
R. Lepigre, M.J. Sammler, K. Memarian, R. Krebbers, D. Dreyer, P. Sewell, Proceedings of the ACM on Programming Languages 6 (2022) 1–32.
[Published Version] View | DOI | Download Published Version (ext.)
 
[3]
2022 | Published | Journal Article | IST-REx-ID: 17504 | OA
Simuliris: A separation logic framework for verifying concurrent program optimizations
L. Gäher, M.J. Sammler, S. Spies, R. Jung, H.-H. Dang, R. Krebbers, J. Kang, D. Dreyer, Proceedings of the ACM on Programming Languages 6 (2022) 1–31.
[Published Version] View | DOI | Download Published Version (ext.)
 
[2]
2021 | Published | Conference Paper | IST-REx-ID: 17505 | OA
RefinedC: Automating the foundational verification of C code with refined ownership types
M.J. Sammler, R. Lepigre, R. Krebbers, K. Memarian, D. Dreyer, D. Garg, in:, Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2021, pp. 158–174.
[Published Version] View | DOI | Download Published Version (ext.)
 
[1]
2019 | Published | Journal Article | IST-REx-ID: 17506 | OA
The high-level benefits of low-level sandboxing
M.J. Sammler, D. Garg, D. Dreyer, T. Litak, Proceedings of the ACM on Programming Languages 4 (2019) 1–32.
[Published Version] View | DOI | Download Published Version (ext.)
 
Marked Publication(s)

Search

Filter Publications

Display / Sort

Export / Embed

Grants


11 Publications

Mark all

[11]
2024 | Published | Journal Article | IST-REx-ID: 17495 | OA
RefinedRust: A type system for high-assurance verification of rust programs
L. Gäher, M.J. Sammler, R. Jung, R. Krebbers, D. Dreyer, Proceedings of the ACM on Programming Languages 8 (2024) 1115–1139.
[Published Version] View | DOI | Download Published Version (ext.)
 
[10]
2024 | Published | Journal Article | IST-REx-ID: 17497 | OA
Quiver: Guided abductive inference of separation logic specifications in coq
S. Spies, L. Gäher, M.J. Sammler, D. Dreyer, Proceedings of the ACM on Programming Languages 8 (2024) 889–913.
[Published Version] View | DOI | Download Published Version (ext.)
 
[9]
2023 | Published | Journal Article | IST-REx-ID: 17498 | OA
Melocoton: A program logic for verified interoperability between OCaml and C
A. Guéneau, J. Hostert, S. Spies, M.J. Sammler, L. Birkedal, D. Dreyer, Proceedings of the ACM on Programming Languages 7 (2023) 716–744.
[Published Version] View | DOI | Download Published Version (ext.)
 
[8]
2023 | Published | Journal Article | IST-REx-ID: 17499 | OA
Conditional contextual refinement
Y. Song, M. Cho, D. Lee, C.-K. Hur, M.J. Sammler, D. Dreyer, Proceedings of the ACM on Programming Languages 7 (2023) 1121–1151.
[Published Version] View | DOI | Download Published Version (ext.)
 
[7]
2023 | Published | Journal Article | IST-REx-ID: 17500 | OA
DimSum: A decentralized approach to multi-language semantics and verification
M.J. Sammler, S. Spies, Y. Song, E. D’Osualdo, R. Krebbers, D. Garg, D. Dreyer, Proceedings of the ACM on Programming Languages 7 (2023) 775–805.
[Published Version] View | DOI | Download Published Version (ext.)
 
[6]
2022 | Published | Journal Article | IST-REx-ID: 17501 | OA
BFF: Foundational and automated verification of bitfield-manipulating programs
F. Zhu, M.J. Sammler, R. Lepigre, D. Dreyer, D. Garg, Proceedings of the ACM on Programming Languages 6 (2022) 1613–1638.
[Published Version] View | DOI | Download Published Version (ext.)
 
[5]
2022 | Published | Conference Paper | IST-REx-ID: 17502 | OA
Islaris: Verification of machine code against authoritative ISA semantics
M.J. Sammler, A. Hammond, R. Lepigre, B. Campbell, J. Pichon-Pharabod, D. Dreyer, D. Garg, P. Sewell, in:, Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2022, pp. 825–840.
[Published Version] View | DOI | Download Published Version (ext.)
 
[4]
2022 | Published | Journal Article | IST-REx-ID: 17503 | OA
VIP: Verifying real-world C idioms with integer-pointer casts
R. Lepigre, M.J. Sammler, K. Memarian, R. Krebbers, D. Dreyer, P. Sewell, Proceedings of the ACM on Programming Languages 6 (2022) 1–32.
[Published Version] View | DOI | Download Published Version (ext.)
 
[3]
2022 | Published | Journal Article | IST-REx-ID: 17504 | OA
Simuliris: A separation logic framework for verifying concurrent program optimizations
L. Gäher, M.J. Sammler, S. Spies, R. Jung, H.-H. Dang, R. Krebbers, J. Kang, D. Dreyer, Proceedings of the ACM on Programming Languages 6 (2022) 1–31.
[Published Version] View | DOI | Download Published Version (ext.)
 
[2]
2021 | Published | Conference Paper | IST-REx-ID: 17505 | OA
RefinedC: Automating the foundational verification of C code with refined ownership types
M.J. Sammler, R. Lepigre, R. Krebbers, K. Memarian, D. Dreyer, D. Garg, in:, Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2021, pp. 158–174.
[Published Version] View | DOI | Download Published Version (ext.)
 
[1]
2019 | Published | Journal Article | IST-REx-ID: 17506 | OA
The high-level benefits of low-level sandboxing
M.J. Sammler, D. Garg, D. Dreyer, T. Litak, Proceedings of the ACM on Programming Languages 4 (2019) 1–32.
[Published Version] View | DOI | Download Published Version (ext.)
 
Marked Publication(s)

Search

Filter Publications

Display / Sort

Export / Embed