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)

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)

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

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)

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)

A Model-Checked I2C Specification. - Lukas Humbel; Daniel David Schwyn; Nora Hossle; Roni Haecki; Melissa Licciardello; Jan Schaer; David A. Cock; Michael Giardino; Timothy Roscoe (SPIN, 2021)

Prepare your video for streaming with Segue. - Melissa Licciardello; Lukas Humbel; Fabian Rohr; Maximilian Grüner; Ankit Singla (CoRR, 2022)

Modern hardware abstractions for firmware. - Lukas Humbel (2022)

[Solution] Prepare your video for streaming with Segue. - Melissa Licciardello; Lukas Humbel; Fabian Rohr; Maximilian Grüner; Ankit Singla (J. Syst. Res., 2022)

Flexible Swapping for the Cloud. - Milan Pandurov; Lukas Humbel; Dmitry Sepp; Adamos Ttofari; Leon Thomm; Do Le Quoc; Siddharth Chandrasekaran; Sharan Santhanam; Chuan Ye; Shai Bergman; Wei Wang; Sven Lundgren; et al. (CoRR, 2024)

Move your code, not your data. - Michael Giardino; Siddharth Gupta 003; Lukas Humbel; René Müller 001; Anirban Nag (HCDS, 2025)