Mothy in the Systems Group at ETH Zürich.
My research focuses applying formal methods at the
hardware-software interface as part of the Sockeye project. Modern
hardware platforms have become immensely complicated, and what is
commonly understood as an “operating system” is but part of a larger
de facto OS. My
research aims to better understand and reduce the complexity of modern
computing platforms with respect to memory addressing.
I am also part of the Enzian
project, researching high-assurance board management controller
software and administering the cluster of working machines.
Topics that I am researching include
- Characterizing and taming the hardware dumpster
fire
- Building robust and formally verified baseboard management
controllers
- Formally modelling and validating the real-world cache coherence
implementation of a ThunderX-1 chip
- Specifying the de facto OS of a production
SoC
Ben Fiedler, Roman Meier, Jasmin Schult, Daniel Schwyn, Timothy
Roscoe
KISV ’23: Proceedings of the 1st Workshop on Kernel Isolation, Safety
and Verification, colocated with SOSP ’23
October 2023
PDF,
Slides,
10.1145/3625275.3625400 - Putting out the hardware dumpster fire
Ben Fiedler, Daniel Schwyn, Constantin Gierczak–Galle, David
Cock, Timothy Roscoe
HotOS ’23: Proceedings of the Workshop on Hot Topics in Operating
Systems
June 2023
PDF,
10.1145/3593856.3595903 - A Formal Proof of the Chandy-Lamport Distributed Snapshot
Algorithm
Ben Fiedler, Dmitriy Traytel
The Archive of Formal Proofs
July 2020
URL
- Informal Methods
ETH Zürich
Fall 2021, Fall 2022, Fall 2023 - Formal Methods and Functional Programming
ETH Zürich
Spring 2020, Spring 2022, Spring 2023 - Introduction to Programming
ETH Zürich
Fall 2019