Running the manual: an approach to high-assurance microkernel development. - Philip Derrin; Kevin Elphinstone; Gerwin Klein; David A. Cock; Manuel M. T. Chakravarty (Haskell, 2006)

Bitfields and Tagged Unions in C: Verification through Automatic Generation. - David A. Cock (VERIFY, 2008)

Secure Microkernels, State Monads and Scalable Refinement. - David A. Cock; Gerwin Klein; Thomas Sewell (TPHOLs, 2008)

seL4: formal verification of an OS kernel. - Gerwin Klein; Kevin Elphinstone; Gernot Heiser; June Andronick; David A. Cock; Philip Derrin; Dhammika Elkaduwe; Kai Engelhardt; Rafal Kolanski; Michael Norrish; Thomas Sewell; Harvey Tuch; et al. (SOSP, 2009)

Mind the Gap. - Simon Winwood; Gerwin Klein; Thomas Sewell; June Andronick; David A. Cock; Michael Norrish (TPHOLs, 2009)

Lyrebird - Assigning Meanings to Machines. - David A. Cock (SSV, 2010)

seL4: formal verification of an operating-system kernel. - Gerwin Klein; June Andronick; Kevin Elphinstone; Gernot Heiser; David A. Cock; Philip Derrin; Dhammika Elkaduwe; Kai Engelhardt; Rafal Kolanski; Michael Norrish; Thomas Sewell; Harvey Tuch; et al. (Commun. ACM, 2010)

Exploitation as an inference problem. - David A. Cock (AISec, 2011)

Verifying Probabilistic Correctness in Isabelle with pGCL - David A. Cock (SSV, 2012)

Practical Probability: Applying pGCL to Lattice Scheduling. - David A. Cock (ITP, 2013)

The Last Mile: An Empirical Study of Timing Channels on seL4. - David A. Cock; Qian Ge 001; Toby C. Murray; Gernot Heiser (CCS, 2014)

From Operational Models to Information Theory; Side Channels in pGCL with Isabelle. - David A. Cock (ITP, 2014)

pGCL for Isabelle. - David A. Cock (Arch. Formal Proofs, 2014)

Leakage in Trustworthy Systems. - David A. Cock (2014)

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 survey of microarchitectural timing attacks and countermeasures on contemporary hardware. - Qian Ge 001; Yuval Yarom; David A. Cock; Gernot Heiser (J. Cryptogr. Eng., 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)

Tackling Hardware/Software co-design from a database perspective. - Gustavo Alonso; Timothy Roscoe; David A. Cock; Mohsen Ewaida; Kaan Kara; Dario Korolija; David Sidler; Zeke Wang (CIDR, 2020)

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)

Declarative Power Sequencing. - Jasmin Schult; Daniel David Schwyn; Michael Giardino; David A. Cock; Reto Achermann; Timothy Roscoe (ACM Trans. Embed. Comput. Syst., 2021)

Enzian: an open, general, CPU/FPGA platform for systems software research. - David A. Cock; Abishek Ramdas; Daniel Schwyn; Michael Giardino; Adam Turowski; Zhenhao He; Nora Hossle; Dario Korolija; Melissa Licciardello; Kristina Martsenko; Reto Achermann; Gustavo Alonso; et al. (ASPLOS, 2022)

ECI: a Customizable Cache Coherency Stack for Hybrid FPGA-CPU Architectures. - Abishek Ramdas; Michael Giardino; Runbin Shi; Adam Turowski; David A. Cock; Gustavo Alonso; Timothy Roscoe (CoRR, 2022)

Putting out the hardware dumpster fire. - Ben Fiedler; Daniel Schwyn; Constantin Gierczak-Galle; David A. Cock; Timothy Roscoe (HotOS, 2023)

Verified Fault Handling for Modern Board Management Controllers. - Ben Fiedler; Zikai Liu; David A. Cock; Timothy Roscoe (FACS, 2024)

Semi-Open-State Testing for in-Silicon Coherent Interconnects. - Jasmin Schult; Ben Fiedler; David A. Cock; Timothy Roscoe (FMCAD, 2024)

Rethinking Programmed I/O for Fast Devices, Cheap Cores, and Coherent Interconnects. - Anastasiia Ruzhanskaia; Pengcheng Xu 005; David A. Cock; Timothy Roscoe (CoRR, 2024)