Seguir
Michael Sammler
Michael Sammler
Email confirmado em mpi-sws.org
Título
Citado por
Citado por
Ano
{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
2292019
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
732021
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
272019
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
232022
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
212022
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
162023
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
142023
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
72023
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
62022
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
12022
Automated and foundational verification of low-level programs
MJ Sammler
Saarländische Universitäts-und Landesbibliothek, 2023
2023
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 DimSum: A Decentralized Approach to Multi-language Semantics and Verification
M SAMMLER, S SPIES, Y SONG, E D’OSUALDO, D GARG, D DREYER
O sistema não pode efectuar a operação agora. Tente mais tarde.
Artigos 1–15