Velosiraptor: Code Synthesis for Memory Translation (to appear).
Reto Achermann, Emily Chu, Ryan Mehri, Ilias Karimalis and Margo Seltzer.
Proceedings of the 30th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'25).
[ .doi ] [ .pdf ] [ .bib ]

Verus: A Practical Foundation for Systems Verification (to appear).
Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jay Lorch, Oded Padon and Bryan Parno.
Proceedings of the 30th Symposium on Operating Systems Principles (SOSP'24).
[ .doi ] [ .pdf ] [ .bib ]

Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems.
Travis Hance, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell and Bryan Parno.
Proceedings of the 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI'23).
[ .doi ] [ .pdf ] [ .bib ]

Enzian: An Open, General, CPU/FPGA Platform for Systems Software Research.
David Cock, Abishek Ramdas, Daniel Schwyn, Michael Giardino, Adam Turowski, Zhenhao He, Nora Hossle, Dario Korolija, Melissa Licciardello, Kristina Martsenko, Reto Achermann, Gustavo Alonso and Timothy Roscoe.
Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'22).
[ .doi ] [ .pdf ] [ .bib ]

Fast Sparse Decision Tree Optimization via Reference Ensembles.
Hayden McTavish, Chudi Zhong, Reto Achermann, Ilias Karimalis, Jacques Chen, Cynthia Rudin and Margo Seltzer.
Proceedings of the Thirty-Sixth AAAI Conference on Artificial Intelligence (AAAI'22).
[ .doi ] [ .pdf ] [ .bib ]

NrOS: Effective Replication and Sharing in an Operating System.
Ankit Bhardwaj, Chinmay Kulkarni, Reto Achermann, Irina Calciu, Sanidhya Kashyap, Ryan Stutsman, Amy Tai and Gerd Zellweger.
Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI'21).
[ .doi ] [ .pdf ] [ .bib ]

Fast Local Page-Tables for Virtualized NUMA Servers with vMitosis.
Ashish Panwar, Reto Achermann, Arkaprava Basu, Abhishek Bhattacharjee, K. Gopinath and Jayneel Gandhi.
Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'21).
[ .doi ] [ .pdf ] [ .bib ]

Mitosis: Transparently Self-Replicating Page-Tables for Large-Memory Machines.
Reto Achermann, Ashish Panwar, Abhishek Bhattacharjee, Timothy Roscoe and Jayneel Gandhi.
Proceedings of the 25th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'20).
[ .doi ] [ .pdf ] [ .bib ]

Physical Addressing on Real Hardware in Isabelle/HOL.
Reto Achermann, Lukas Humbel, David Cock and Timothy Roscoe.
Proceedings of the 9th International Conference on Interactive Theorem Proving (ITP'18).
[ .doi ] [ .pdf ] [ .bib ]

SpaceJMP: Programming with Multiple Virtual Address Spaces.
Izzat El Hajj, Alexander Merritt, Gerd Zellweger, Dejan Milojicic, Reto Achermann, Paolo Faraboschi, Wen-mei Hwu, Timothy Roscoe and Karsten Schwan.
Proceedings of the 21st International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'16).
[ .doi ] [ .pdf ] [ .bib ]

Machine-aware Atomic Broadcast Trees for Multicores.
Stefan Kaestle, Reto Achermann, Roni Haecki, Moritz Hoffmann, Sabela Ramos and Timothy Roscoe.
Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI'16).
[ .doi ] [ .pdf ] [ .bib ]

Shoal: Smart Allocation and Replication of Memory for Parallel Programs.
Stefan Kaestle, Reto Achermann, Timothy Roscoe and Tim Harris.
Proceedings of the 2015 USENIX Conference on Usenix Annual Technical Conference (USENIX ATC'15).
[ .doi ] [ .pdf ] [ .bib ]

Declarative Power Sequencing.
Jasmin Schult, Daniel Schwyn, Michael Giardino, David Cock, Reto Achermann and Timothy Roscoe.
ACM TECS.
[ .doi ] [ .pdf ] [ .bib ]

Memory-Side Protection With a Capability Enforcement Co-Processor.
Leonid Azriel, Lukas Humbel, Reto Achermann, Alex Richardson, Moritz Hoffmann, Avi Mendelson, Timothy Roscoe, Robert N. M. Watson, Paolo Faraboschi and Dejan Milojicic.
ACM TACO.
[ .doi ] [ .pdf ] [ .bib ]

Why write address translation OS code yourself when you can synthesize it?.
Reto Achermann, Ilias Karimalis and Margo Seltzer.
Proceedings of the 19th Workshop on Hot Topics in Operating Systems (HotOS'23).
[ .doi ] [ .pdf ] [ .bib ]

Beyond isolation: OS verification as a foundation for correct applications.
Matthias Brun, Reto Achermann, Tej Chajed, Jon Howell, Gerd Zellweger and Andrea Lattuada.
Proceedings of the 19th Workshop on Hot Topics in Operating Systems (HotOS'23).
[ .doi ] [ .pdf ] [ .bib ]

Synthesizing Device Drivers with Ghost Writer.
Bingyao Wang, Sepehr Noorafshan, Reto Achermann and Margo Seltzer.
Proceedings of the 12th Workshop on Programming Languages and Operating Systems (PLOS'23).
[ .doi ] [ .pdf ] [ .bib ]

Cache-Coherent Accelerators for Persistent Memory Crash Consistency.
Ankit Bhardwaj, Todd Thornley, Vinita Pawar, Reto Achermann, Gerd Zellweger and Ryan Stutsman.
Proceedings of the 14th ACM Workshop on Hot Topics in Storage and File Systems (HotStorage'22).
[ .doi ] [ .pdf ] [ .bib ]

Mmapx: Uniform Memory Protection in a Heterogeneous World.
Reto Achermann, David Cock, Roni Haecki, Nora Hossle, Lukas Humbel, Timothy Roscoe and Daniel Schwyn.
Proceedings of the Workshop on Hot Topics in Operating Systems (HotOS'21).
[ .doi ] [ .pdf ] [ .bib ]

Generating Correct Initial Page Tables from Formal Hardware Descriptions.
Reto Achermann, David Cock, Roni Haecki, Nora Hossle, Lukas Humbel, Timothy Roscoe and Daniel Schwyn.
Proceedings of the 11th Workshop on Programming Languages and Operating Systems (PLOS'21).
[ .doi ] [ .pdf ] [ .bib ]

Separating Translation from Protection in Address Spaces with Dynamic Remapping.
Reto Achermann, Chris Dalton, Paolo Faraboschi, Moritz Hoffmann, Dejan Milojicic, Geoffrey Ndu, Alexander Richardson, Timothy Roscoe, Adrian L. Shaw and Robert N. M. Watson.
Proceedings of the 16th Workshop on Hot Topics in Operating Systems (HotOS'17).
[ .doi ] [ .pdf ] [ .bib ]

Towards Correct-by-Construction Interrupt Routing on Real Hardware.
Lukas Humbel, Reto Achermann, David Cock and Timothy Roscoe.
Proceedings of the 9th Workshop on Programming Languages and Operating Systems (PLOS'17).
[ .doi ] [ .pdf ] [ .bib ]

Formalizing Memory Accesses and Interrupts.
Reto Achermann, Lukas Humbel, David Cock and Timothy Roscoe.
Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems (MARS'17).
[ .doi ] [ .pdf ] [ .bib ]

Not Your Parents' Physical Address Space.
Simon Gerber, Gerd Zellweger, Reto Achermann, Kornilios Kourtis, Timothy Roscoe and Dejan Milojicic.
Proceedings of the 15th USENIX Conference on Hot Topics in Operating Systems (HotOS'15).
[ .doi ] [ .pdf ] [ .bib ]

Transparent Self-Replicating Page Tables in Computing Systems.
Reto Achermann and Jayneel Gandhi.
US11573904B2. United States of America.
[ .doi ] [ .www ] [ .bib ]

Interoperable capabilities.
Reto Achermann, Maurice Bailleu, Dejan S. Milojicic and Gabriel Parmer.
US20170329526A1. United States of America.
[ .doi ] [ .www ] [ .bib ]

Memory management with versioning of objects.
Izzat El Hajj, Alexander Merritt, Gerd Zellweger, Dejan S. Milojicic and Reto Achermann.
WO2017131789A1. International.
[ .doi ] [ .www ] [ .bib ]

OSmosis: No more Déjà vu in OS isolation.
Sidhartha Agrawal, Reto Achermann and Margo Seltzer.
arXiv Preprint.
[ .doi ] [ .pdf ] [ .bib ]

Secure Memory Management on Modern Hardware.
Reto Achermann, Nora Hossle, Lukas Humbel, Daniel Schwyn, David Cock and Timothy Roscoe.
arXiv Preprint.
[ .doi ] [ .pdf ] [ .bib ]

A Least-Privilege Memory Protection Model for Modern Hardware.
Reto Achermann, Nora Hossle, Lukas Humbel, Daniel Schwyn, David Cock and Timothy Roscoe.
arXiv Preprint.
[ .doi ] [ .pdf ] [ .bib ]

CleanQ: a lightweight, uniform, formally specified interface for intra-machine data transfer.
Roni Haecki, Lukas Humbel, Reto Achermann, David Cock, Daniel Schwyn and Timothy Roscoe.
arXiv Preprint.
[ .doi ] [ .pdf ] [ .bib ]

Cichlid: Explicit physical memory management for large machines.
Simon Gerber, Gerd Zellweger, Reto Achermann, Moritz Hoffmann, Kornilios Kourtis, Timothy Roscoe and Dejan Milojicic.
arXiv Preprint.
[ .doi ] [ .pdf ] [ .bib ]

On Memory Addressing.
Reto Achermann.
Department of Computer Science, ETH Zurich.
[ .doi ] [ .pdf ] [ .bib ]

Message Passing and Bulk Transport on Heterogenous Multiprocessors.
Reto Achermann.
Department of Computer Science, ETH Zurich.
[ .doi ] [ .pdf ] [ .bib ]

Barrelfish USB Subsystem.
Reto Achermann.
Department of Computer Science, ETH Zurich.
[ .doi ] [ .pdf ] [ .bib ]