David A. Cock

According to our database, David A. Cock authored at least 31 papers between 2006 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

Rethinking Programmed I/O for Fast Devices, Cheap Cores, and Coherent Interconnects.

Anastasiia Ruzhanskaia, Pengcheng Xu, David A. Cock, Timothy Roscoe

CoRR, 2024

Verified Fault Handling for Modern Board Management Controllers.

Ben Fiedler, Zikai Liu, David A. Cock, Timothy Roscoe

Proceedings of the Formal Aspects of Component Software - 20th International Conference, 2024

2023

Putting out the hardware dumpster fire.

Ben Fiedler, Daniel Schwyn, Constantin Gierczak-Galle, David A. Cock, Timothy Roscoe

Proceedings of the 19th Workshop on Hot Topics in Operating Systems, 2023

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

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, Timothy Roscoe

Proceedings of the ASPLOS '22: 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Lausanne, Switzerland, 28 February 2022, 2022

2021

Declarative Power Sequencing.

Jasmin Schult, Daniel David Schwyn, Michael Giardino, David A. Cock, Reto Achermann, Timothy Roscoe

ACM Trans. Embed. Comput. Syst., 2021

A Model-Checked I²C Specification.

Lukas Humbel, Daniel David Schwyn, Nora Hossle, Roni Haecki, Melissa Licciardello, Jan Schaer, David A. Cock, Michael Giardino, Timothy Roscoe

Proceedings of the Model Checking Software - 27th International Symposium, 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

Proceedings of the PLOS '21: Proceedings of the 11th Workshop on Programming Languages and Operating Systems, 2021

mmapx: uniform memory protection in a heterogeneous world.

Reto Achermann, David A. Cock, Roni Haecki, Nora Hossle, Lukas Humbel, Timothy Roscoe, Daniel David Schwyn

Proceedings of the HotOS '21: Workshop on Hot Topics in Operating Systems, 2021

2020

Secure Memory Management on Modern Hardware.

Reto Achermann, Nora Hossle, Lukas Humbel, Daniel David Schwyn, David A. Cock, Timothy Roscoe

CoRR, 2020

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

Proceedings of the 10th Conference on Innovative Data Systems Research, 2020

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

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

2018

A survey of microarchitectural timing attacks and countermeasures on contemporary hardware.

Qian Ge, Yuval Yarom, David A. Cock, Gernot Heiser

J. Cryptogr. Eng., 2018

Physical Addressing on Real Hardware in Isabelle/HOL.

Reto Achermann, Lukas Humbel, David A. Cock, Timothy Roscoe

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

2017

Formalizing Memory Accesses and Interrupts.

Reto Achermann, Lukas Humbel, David A. Cock, Timothy Roscoe

Proceedings of the Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems, 2017

Towards Correct-by-Construction Interrupt Routing on Real Hardware.

Lukas Humbel, Reto Achermann, David A. Cock, Timothy Roscoe

Proceedings of the 9th Workshop on Programming Languages and Operating Systems, 2017

2014

Leakage in Trustworthy Systems.

David A. Cock

PhD thesis, 2014

pGCL for Isabelle.

David A. Cock

Arch. Formal Proofs, 2014

From Operational Models to Information Theory; Side Channels in pGCL with Isabelle.

David A. Cock

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

The Last Mile: An Empirical Study of Timing Channels on seL4.

David A. Cock, Qian Ge, Toby C. Murray, Gernot Heiser

Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, 2014

2013

Practical Probability: Applying pGCL to Lattice Scheduling.

David A. Cock

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012

Verifying Probabilistic Correctness in Isabelle with pGCL

David A. Cock

Proceedings of the Proceedings Seventh Conference on Systems Software Verification, 2012

2011

Exploitation as an inference problem.

David A. Cock

Proceedings of the 4th ACM Workshop on Security and Artificial Intelligence, 2011

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, Simon Winwood

Commun. ACM, 2010

Lyrebird - Assigning Meanings to Machines.

David A. Cock

Proceedings of the 5th International Workshop on Systems Software Verification, 2010

2009

Mind the Gap.

Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David A. Cock, Michael Norrish

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

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, Simon Winwood

Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, 2009

2008

Secure Microkernels, State Monads and Scalable Refinement.

David A. Cock, Gerwin Klein, Thomas Sewell

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

Bitfields and Tagged Unions in C: Verification through Automatic Generation.

David A. Cock

Proceedings of the 5th International Verification Workshop in connection with IJCAR 2008, 2008

2006

Running the manual: an approach to high-assurance microkernel development.

Philip Derrin, Kevin Elphinstone, Gerwin Klein, David A. Cock, Manuel M. T. Chakravarty

Proceedings of the ACM SIGPLAN Workshop on Haskell, 2006