Publications
- Specifying the de-facto OS of a production SoC, Ben Fiedler, Roman Meier, Jasmin Schult, Daniel Schwyn, Timothy Roscoe. Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification (KISV ‘23), Association for Computing Machinery, New York, NY, USA, October 2023, pp. 18-25. [PDF] [ACM]
- Putting out the hardware dumpster fire, 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, pp. 46-52. [PDF] [ACM]
- Declarative Power Sequencing, Jasmin Schult, Daniel Schwyn, Michael Giardino, David Cock, Reto Achermann, Timothy Roscoe. ACM Transactions on Embedded Computing Systems, ACM Press, New York, NY, USA, vol. 20, no. 5s, October 2021, pp. 1–21. [PDF] [ACM]
- A model-checked I2C specification, Lukas Humbel, Daniel Schwyn, Nora Hossle, Roni Häcki, Melissa Licciardello, Jan Schär, David Cock, Michael Giardino, Timothy Roscoe. Proceedings of the 27th International SPIN Symposium on Model Checking of Software, July 2021. [PDF] [ACM]
- mmapx: uniform memory protection in a heterogeneous world, Reto Achermann, David Cock, Roni Haecki, Nora Hossle, Lukas Humbel, Timothy Roscoe, Daniel Schwyn. HotOS ‘21: Proceedings of the Workshop on Hot Topics in Operating Systems, June 2021, pp. 159–166. [PDF] [Video] [ACM]
- Generating Correct Initial Page Tables from Formal Hardware Descriptions, Reto Achermann, David Cock, Roni Haecki, Nora Hossle, Lukas Humbel, Timothy Roscoe, Daniel Schwyn. Proceedings of the 11th Workshop on Programming Languages and Operating Systems, Association for Computing Machinery, New York, NY, USA, 2021, pp. 69–-75. [PDF] [ACM]
- Physical Addressing on Real Hardware in Isabelle/HOL, Reto Achemann, Lukas Humbel, David Cock, Timothy Roscoe. 9th International Conference on Interactive Theorem Proving, Oxford, United Kingdom, July 2018. [PDF] [Springer]
- Towards Correct-by-Construction Interrupt Routing on Real Hardware, Lukas Humbel, Reto Achemann, David Cock, Timothy Roscoe. 9th Workshop on Programming Languages and Operating Systems (PLOS 2017), Shanghai, China, October 2017. [PDF] [ACM]
- 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, Robert N. M. Watson. Proceedings of the 16th Workshop on Hot Topics in Operating Systems (HotOS-XVI), Whistler, BC, Canada, May 2017. [PDF] [ACM]
- Formalizing Memory Accesses and Interrupts, Reto Achermann, Lukas Humbel, David Cock, Timothy Roscoe. 2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017), Uppsala, Sweden, April 2017. [PDF]
- Not Your Parents’ Physical Address Space, Simon Gerber, Gerd Zellweger, Reto Achermann, Kornilios Kourtis, Timothy Roscoe, Dejan Milojicic. Proceedings of the 15th Workshop on Hot Topics in Operating Systems (HotOS-XV), Kartause Ittingen, Switzerland, May 2015. [PDF] [ACM]