New faculty hire Dr. Reto Achermann brings his expertise in computer systems
This July, the UBC Department of Computer Science (CS) was thrilled to hire Dr. Reto Achermann, a rising star in Computer Systems
The department of Computer Science extends a heartfelt welcome to Dr. Achermann, one of our newest faculty members. Dr. Achermann's research encompasses many areas of computer systems: memory and storage systems, hardware platforms, formal specification and verification, device drivers, and software synthesis He applies formal methods to ensure that operating systems are correct and secure, so that we can trust them to run sensitive applications such as your banking application or personal email. His work explores how to ensure correctness and privacy without sacrificing efficiency.
Finding inspiration in a Commodore 64
Dr. Achermann’s passion for computer science began at a young age in a small town near Lucerne, Switzerland. He fondly remembers watching his father tinkering with his family’s Commodore 64, a vintage personal computer. "I think my dad still has it in the attic, along with some 5.25 inch floppy disks," he laughs. As a child, Reto spent many hours experimenting, programming, playing games, and exploring the capabilities of their family computer.
It was the beginning of a lifelong pursuit.
Achermann’s curiosity about computers eventually led him to study computer science formally. After completing his undergraduate degree in Switzerland, he pursued his Master’s and Doctorate at ETH Zurich under the supervision of Dr. Timothy Roscoe, an expert in operating systems.
During this period, Reto’s work centered on understanding how memory operates within computer systems, a topic that laid the foundation for his current research. Following his Doctorate, Reto joined UBC for his postdoc where he began applying advanced program synthesis techniques—automatically generating programs that configure machines based on a formal model—an area that piqued his interest in formal methods.
‘Formal Methods:' a short definition
Formal Methods is a set of tools used in computer science to specify and prove the correctness of computer systems.
Dr. Achermann explains Formal Methods, “We often make assumptions in our heads about computer systems that we don’t write down. Formal Methods requires you to write them down and provide proof that the code actually satisfies them.” Achermann points out that this approach is crucial when designing operating systems, as there must be a seamless interaction with the hardware while ensuring that various apps operate in isolation for privacy and security reasons (e.g., banking apps).
Currently, Reto is collaborating with colleagues to explore how formal systems can provide this isolation between applications or ‘agents.’ Isolation prevents interference between programs running simultaneously, which is especially important when dealing with sensitive information or complex tasks that require concurrency. More specifically, multiple applications or programs may need to run at once, but none of them should access the resources of the others while doing so. Reto and his team are working on guaranteeing this isolation by proving the ‘correctness’ of these systems, even when hardware configurations are altered.
The passion is in the mystery
For Dr. Achermann, the most exciting aspect of his work is building systems that work as intended yet aren’t immediately apparent. “When you build something new for the first time and see some promising output, it’s an incredible feeling,” he says. Achermann thrives on the challenge of using different tools to ensure a system performs well even when it doesn’t initially appear to do so. “The computer might come up with a solution that seems odd, but when you realize it actually works, it’s liberating and fascinating.”
This passion for system-building and problem-solving is what drives Reto in his research. Whether he’s developing new operating system configurations or applying formal methods to prove the correctness of system software, he is dedicated to ensuring the technology we rely upon every day operates efficiently and securely.
Operating in a great climate
Reto expressed his excitement in joining the UBC community and climate across multiple levels. He is drawn both to the supportive and collaborative environment of the Computer Science Department, and the actual climate of the location.
“There’s a really good climate here all round,” he says. “Vancouver is a beautiful place to live. In addition, the research interactions I’ve had so far have been very fruitful. The culture within the department is welcoming and friendly, with many opportunities for collaboration between different labs.” Reto says the atmosphere of support and collegiality has been key for him in terms of fostering progress in his research and developing strong working relationships with his colleagues.
Dr. Achermann was already a CS departmental member as a postdoctoral fellow working in the Systopia Lab alongside Dr. Margo Seltzer when he decided to apply for the new tenure-track position. His contributions had already been phenomenal. He received the Faculty of Science ‘Excellence in Service’ award in March of 2024. This award honours his work in developing a new undergraduate course for the department on operating systems, 436A: Operating Systems Design & Implementation. By all accounts, his efforts in creating and sustaining this course have had a significant impact on students – both graduates and undergraduates – in fostering a collaborative and supportive learning environment.
Reto has also been a mentor to many students, offering technical advice, personal support, and invaluable guidance. His dedication to nurturing the academic and personal growth of students makes him an integral part of the UBC community.
When he’s not immersed in research or teaching, Dr. Achermann enjoys spending time outdoors, particularly hiking and visiting national parks. He begins his day with an early morning workout and enjoys baking and cooking in his free time.
In the spirit of life imitating science: Reto even applies a computer science-related principle to his daily routine—particularly his laundry! He follows the FIFO (First In, First Out) policy, with respect to when his clothes are being hung in the closet). Washed clothes go in on the left side, and he takes his clothes to wear from the right side, ensuring the wardrobe stays organized.
Looking ahead
Dr. Achermann is excited to make more contributions to UBC’s Computer Science department, both in research and teaching. With his passion for building systems that work, a dedication to formal methods, and enthusiasm for mentoring students, he’s sure to make a lasting impact on both the department and the field of computer science.