| {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 | 94 | 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 | 18 | 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 | 18 | 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 | 3 | 2022 |
| Islaris: Verification of Machine Code Against Authoritative ISA Semantics M Sammler, A Hammond, R Lepigre, B Campbell, J Pichon-Pharabod, ... 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2022 | 1 | 2022 |
| 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 | | 2022 |
| Simuliris: A Separation Logic Framework for Verifying rent Program Optimizations L Gähler, M Sammler, S Spies, R Jung, HH Dang, RJ Krebbers, J Kang, ... | | 2022 |
| 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 Gaher, M Sammler, S Spies, R Jung, HH Dang, RJ Krebbers, J Kang, ... Zenodo, 2021 | | 2021 |
| date: 2022-01-10T21: 24: 28Z pdf: PDFVersion: 1.7 pdf: docinfo: title: VIP: Verifying Real-World C Idioms with Integer-Pointer Casts xmp: CreatorTool: LaTeX with acmart 2021/05 … R Lepigre, M Sammler, K Memarian, R Krebbers, D Dreyer, P Sewell | | |
