Not Your Parents' Physical Address Space. - Simon Gerber; Gerd Zellweger; Reto Achermann; Kornilios Kourtis; Timothy Roscoe; Dejan S. Milojicic (HotOS, 2015)

Shoal: Smart Allocation and Replication of Memory For Parallel Programs. - Stefan Kaestle; Reto Achermann; Timothy Roscoe; Tim Harris 001 (USENIX ATC, 2015)

SpaceJMP: Programming with Multiple Virtual Address Spaces. - Izzat El Hajj; Alexander Merritt; Gerd Zellweger; Dejan S. Milojicic; Reto Achermann; Paolo Faraboschi; Wen-mei W. Hwu; Timothy Roscoe; Karsten Schwan (ASPLOS, 2016)

Machine-Aware Atomic Broadcast Trees for Multicores. - Stefan Kaestle; Reto Achermann; Roni Haecki; Moritz Hoffmann 001; Sabela Ramos; Timothy Roscoe (OSDI, 2016)

Separating Translation from Protection in Address Spaces with Dynamic Remapping. - Reto Achermann; Chris I. Dalton; Paolo Faraboschi; Moritz Hoffmann 001; Dejan S. Milojicic; Geoffrey Ndu; Alexander Richardson 001; Timothy Roscoe; Adrian L. Shaw; Robert N. M. Watson (HotOS, 2017)

Towards Correct-by-Construction Interrupt Routing on Real Hardware. - Lukas Humbel; Reto Achermann; David A. Cock; Timothy Roscoe (PLOS@SOSP, 2017)

Formalizing Memory Accesses and Interrupts. - Reto Achermann; Lukas Humbel; David A. Cock; Timothy Roscoe (MARS@ETAPS, 2017)

Physical Addressing on Real Hardware in Isabelle/HOL. - Reto Achermann; Lukas Humbel; David A. Cock; Timothy Roscoe (ITP, 2018)

A Least-Privilege Memory Protection Model for Modern Hardware. - Reto Achermann; Nora Hossle; Lukas Humbel; Daniel David Schwyn; David A. Cock; Timothy Roscoe (CoRR, 2019)

Cichlid: Explicit physical memory management for large machines. - Simon Gerber; Gerd Zellweger; Reto Achermann; Moritz Hoffmann 001; Kornilios Kourtis; Timothy Roscoe; Dejan S. Milojicic (CoRR, 2019)

CleanQ: a lightweight, uniform, formally specified interface for intra-machine data transfer. - Roni Haecki; Lukas Humbel; Reto Achermann; David A. Cock; Daniel David Schwyn; Timothy Roscoe (CoRR, 2019)

Memory-Side Protection With a Capability Enforcement Co-Processor. - Leonid Azriel; Lukas Humbel; Reto Achermann; Alex Richardson 001; Moritz Hoffmann 001; Avi Mendelson; Timothy Roscoe; Robert N. M. Watson; Paolo Faraboschi; Dejan S. Milojicic (ACM Trans. Archit. Code Optim., 2019)

Mitosis: Transparently Self-Replicating Page-Tables for Large-Memory Machines. - Reto Achermann; Ashish Panwar; Abhishek Bhattacharjee; Timothy Roscoe; Jayneel Gandhi (ASPLOS, 2020)

Secure Memory Management on Modern Hardware. - Reto Achermann; Nora Hossle; Lukas Humbel; Daniel David Schwyn; David A. Cock; Timothy Roscoe (CoRR, 2020)

On Memory Addressing. - Reto Achermann (2020)

Fast local page-tables for virtualized NUMA servers with vMitosis. - Ashish Panwar; Reto Achermann; Arkaprava Basu; Abhishek Bhattacharjee; K. Gopinath; Jayneel Gandhi (ASPLOS, 2021)

mmapx: uniform memory protection in a heterogeneous world. - Reto Achermann; David A. Cock; Roni Haecki; Nora Hossle; Lukas Humbel; Timothy Roscoe; Daniel David Schwyn (HotOS, 2021)

NrOS: Effective Replication and Sharing in an Operating System. - Ankit Bhardwaj; Chinmay Kulkarni 002; Reto Achermann; Irina Calciu; Sanidhya Kashyap; Ryan Stutsman; Amy Tai; Gerd Zellweger (OSDI, 2021)

Generating correct initial page tables from formal hardware descriptions. - Reto Achermann; David A. Cock; Roni Haecki; Nora Hossle; Lukas Humbel; Timothy Roscoe; Daniel David Schwyn (PLOS@SOSP, 2021)

Declarative Power Sequencing. - Jasmin Schult; Daniel David Schwyn; Michael Giardino; David A. Cock; Reto Achermann; Timothy Roscoe (ACM Trans. Embed. Comput. Syst., 2021)

Fast Sparse Decision Tree Optimization via Reference Ensembles. - Hayden McTavish; Chudi Zhong; Reto Achermann; Ilias Karimalis; Jacques Chen; Cynthia Rudin; Margo I. Seltzer (AAAI, 2022)

Enzian: an open, general, CPU/FPGA platform for systems software research. - David A. Cock; Abishek Ramdas; Daniel Schwyn; Michael Giardino; Adam Turowski; Zhenhao He; Nora Hossle; Dario Korolija; Melissa Licciardello; Kristina Martsenko; Reto Achermann; Gustavo Alonso; et al. (ASPLOS, 2022)

Cache-coherent accelerators for persistent memory crash consistency. - Ankit Bhardwaj; Todd Thornley; Vinita Pawar; Reto Achermann; Gerd Zellweger; Ryan Stutsman (HotStorage, 2022)

Beyond isolation: OS verification as a foundation for correct applications. - Matthias Brun 002; Reto Achermann; Tej Chajed; Jon Howell; Gerd Zellweger; Andrea Lattuada 001 (HotOS, 2023)

Why write address translation OS code yourself when you can synthesize it? - Reto Achermann; Ilias Karimalis; Margo I. Seltzer (HotOS, 2023)

Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems. - Travis Hance; Yi Zhou 025; Andrea Lattuada 001; Reto Achermann; Alex Conway 001; Ryan Stutsman; Gerd Zellweger; Chris Hawblitzel; Jon Howell; Bryan Parno (OSDI, 2023)

Synthesizing Device Drivers with Ghost Writer. - Bingyao Wang; Sepehr Noorafshan; Reto Achermann; Margo I. Seltzer (PLOS@SOSP, 2023)

OSmosis: No more Déjà vu in OS isolation. - Sidhartha Agrawal; Reto Achermann; Margo I. Seltzer (CoRR, 2023)

Verus: A Practical Foundation for Systems Verification. - Andrea Lattuada 001; Travis Hance; Jay Bosamiya; Matthias Brun 002; Chanhee Cho; Hayley LeBlanc; Pranav Srinivasan; Reto Achermann; Tej Chajed; Chris Hawblitzel; Jon Howell; Jacob R. Lorch; et al. (SOSP, 2024)

Velosiraptor: Code Synthesis for Memory Translation. - Reto Achermann; Em Chu; Ryan Mehri; Ilias Karimalis; Margo I. Seltzer (ASPLOS (2), 2025)

Velosiraptor: Code Synthesis for Memory Translation. - Reto Achermann; Emily Chu; Ryan Mehri; Ilias Karimalis; Margo I. Seltzer (Zenodo, 2025)