| {ERIM}: Secure, Efficient In-process Isolation with Protection Keys ({{{{{MPK}}}}}) A Vahldiek-Oberwagner, E Elnikety, NO Duarte, M Sammler, P Druschel, ... 28th USENIX Security Symposium (USENIX Security 19), 1221-1238, 2019 | 309 | 2019 |
| RefinedC: automating the foundational verification of C code with refined ownership types M Sammler, R Lepigre, R Krebbers, K Memarian, D Dreyer, D Garg Proceedings of the 42nd ACM SIGPLAN International Conference on Programming …, 2021 | 104 | 2021 |
| The high-level benefits of low-level sandboxing M Sammler, D Garg, D Dreyer, T Litak Proceedings of the ACM on Programming Languages 4 (POPL), 1-32, 2019 | 36 | 2019 |
| Simuliris: a separation logic framework for verifying concurrent program optimizations L Gäher, M Sammler, S Spies, R Jung, HH Dang, R Krebbers, J Kang, ... Proceedings of the ACM on Programming Languages 6 (POPL), 1-31, 2022 | 32 | 2022 |
| Conditional contextual refinement Y Song, M Cho, D Lee, CK Hur, M Sammler, D Dreyer Proceedings of the ACM on Programming Languages 7 (POPL), 1121-1151, 2023 | 28 | 2023 |
| Islaris: verification of machine code against authoritative ISA semantics M Sammler, A Hammond, R Lepigre, B Campbell, J Pichon-Pharabod, ... Proceedings of the 43rd ACM SIGPLAN International Conference on Programming …, 2022 | 27 | 2022 |
| Dimsum: A decentralized approach to multi-language semantics and verification M Sammler, S Spies, Y Song, E D'Osualdo, R Krebbers, D Garg, D Dreyer Proceedings of the ACM on Programming Languages 7 (POPL), 775-805, 2023 | 24 | 2023 |
| Melocoton: A program logic for verified interoperability between ocaml and c A Guéneau, J Hostert, S Spies, M Sammler, L Birkedal, D Dreyer Proceedings of the ACM on Programming Languages 7 (OOPSLA2), 716-744, 2023 | 20 | 2023 |
| VIP: verifying real-world C idioms with integer-pointer casts R Lepigre, M Sammler, K Memarian, R Krebbers, D Dreyer, P Sewell Proceedings of the ACM on Programming Languages 6 (POPL), 1-32, 2022 | 15 | 2022 |
| RefinedRust: A Type System for High-Assurance Verification of Rust Programs L GÄHER, M SAMMLER, R JUNG, R KREBBERS, D DREYER | 8 | 2024 |
| BFF: foundational and automated verification of bitfield-manipulating programs F Zhu, M Sammler, R Lepigre, D Dreyer, D Garg Proceedings of the ACM on Programming Languages 6 (OOPSLA2), 1613-1638, 2022 | 2 | 2022 |
| Formal Foundations for Translational Separation Logic Verifiers (extended version) T Dardinier, M Sammler, G Parthasarathy, AJ Summers, P Müller arXiv preprint arXiv:2407.20002, 2024 | 1 | 2024 |
| Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq S Spies, L Gäher, M Sammler, D Dreyer Proceedings of the ACM on Programming Languages 8 (PLDI), 889-913, 2024 | 1 | 2024 |
| Automated and foundational verification of low-level programs MJ Sammler Saarländische Universitäts-und Landesbibliothek, 2023 | 1 | 2023 |
| Formal Foundations for Translational Separation Logic Verifiers T Dardinier, M Sammler, G Parthasarathy, AJ Summers, P Müller Proceedings of the ACM on Programming Languages 9 (POPL), 569-599, 2025 | | 2025 |
| Program Logics à la Carte M Vistrup, M Sammler, R Jung Proceedings of the ACM on Programming Languages 9 (POPL), 300-331, 2025 | | 2025 |
| Artifact and Appendix of" RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types" M Sammler, R Lepigre, RJ Krebbers, K Memarian, D Dreyer, D Garg Zenodo, 2021 | | 2021 |
| Artifact and Appendix of" VIP: Verifying Real-World C Idioms with Integer-Pointer Casts" R Lepigre, M Sammler, K Memarian, R Krebbers, D Dreyer, P Sewell Zenodo, 2021 | | 2021 |
| Coq development for" Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations" L Gäher, M Sammler, S Spies, R Jung, HH Dang, RJ Krebbers, J Kang, ... Zenodo, 2021 | | 2021 |
| Appendix of Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq S SPIES, L GÄHER, M SAMMLER, D DREYER | | |
