default search action
David A. Cock
Person information
- affiliation: ETH Zurich, Zürich, Switzerland
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [c21]Ben Fiedler
, Zikai Liu
Verified Fault Handling for Modern Board Management Controllers. FACS 2024: 21-38 - [i6]Anastasiia Ruzhanskaia, Pengcheng Xu
Rethinking Programmed I/O for Fast Devices, Cheap Cores, and Coherent Interconnects. CoRR abs/2409.08141 (2024) - 2023
- [c20]Ben Fiedler
Putting out the hardware dumpster fire. HotOS 2023: 46-52 - 2022
- [c19]David A. Cock
Enzian: an open, general, CPU/FPGA platform for systems software research. ASPLOS 2022: 434-451 - [i5]Abishek Ramdas, Michael Giardino, Runbin Shi, Adam Turowski, David A. Cock, Gustavo Alonso, Timothy Roscoe:
ECI: a Customizable Cache Coherency Stack for Hybrid FPGA-CPU Architectures. CoRR abs/2208.07124 (2022) - 2021
- [j4]Jasmin Schult, Daniel David Schwyn
Declarative Power Sequencing. ACM Trans. Embed. Comput. Syst. 20(5s): 84:1-84:21 (2021) - [c18]Reto Achermann, David A. Cock
mmapx: uniform memory protection in a heterogeneous world. HotOS 2021: 159-166 - [c17]Reto Achermann, David A. Cock
Generating correct initial page tables from formal hardware descriptions. PLOS@SOSP 2021: 69-75 - [c16]Lukas Humbel
A Model-Checked I2C Specification. SPIN 2021: 177-193 - 2020
- [c15]Gustavo Alonso, Timothy Roscoe, David A. Cock, Mohsen Ewaida, Kaan Kara, Dario Korolija, David Sidler, Zeke Wang:
Tackling Hardware/Software co-design from a database perspective. CIDR 2020 - [i4]Reto Achermann, Nora Hossle, Lukas Humbel, Daniel David Schwyn
Secure Memory Management on Modern Hardware. CoRR abs/2009.02737 (2020)
2010 – 2019
- 2019
- [i3]Reto Achermann, Nora Hossle, Lukas Humbel, Daniel David Schwyn
A Least-Privilege Memory Protection Model for Modern Hardware. CoRR abs/1908.08707 (2019) - [i2]Roni Haecki, Lukas Humbel, Reto Achermann, David A. Cock, Daniel David Schwyn
CleanQ: a lightweight, uniform, formally specified interface for intra-machine data transfer. CoRR abs/1911.08773 (2019) - 2018
- [j3]Qian Ge, Yuval Yarom, David A. Cock
A survey of microarchitectural timing attacks and countermeasures on contemporary hardware. J. Cryptogr. Eng. 8(1): 1-27 (2018) - [c14]Reto Achermann, Lukas Humbel
Physical Addressing on Real Hardware in Isabelle/HOL. ITP 2018: 1-19 - 2017
- [c13]Lukas Humbel, Reto Achermann, David A. Cock
Towards Correct-by-Construction Interrupt Routing on Real Hardware. PLOS@SOSP 2017: 8-14 - [c12]Reto Achermann, Lukas Humbel, David A. Cock
Formalizing Memory Accesses and Interrupts. MARS@ETAPS 2017: 66-116 - 2016
- [i1]Qian Ge, Yuval Yarom, David A. Cock, Gernot Heiser:
A Survey of Microarchitectural Timing Attacks and Countermeasures on Contemporary Hardware. IACR Cryptol. ePrint Arch. 2016: 613 (2016) - 2014
- [b1]David A. Cock:
Leakage in Trustworthy Systems. University of New South Wales, Sydney, Australia, 2014 - [j2]David A. Cock:
pGCL for Isabelle. Arch. Formal Proofs 2014 (2014) - [c11]David A. Cock
The Last Mile: An Empirical Study of Timing Channels on seL4. CCS 2014: 570-581 - [c10]David A. Cock
From Operational Models to Information Theory; Side Channels in pGCL with Isabelle. ITP 2014: 177-192 - 2013
- [c9]David A. Cock
Practical Probability: Applying pGCL to Lattice Scheduling. ITP 2013: 311-327 - 2012
- [c8]David A. Cock
Verifying Probabilistic Correctness in Isabelle with pGCL. SSV 2012: 167-178 - 2011
- [c7]David A. Cock
Exploitation as an inference problem. AISec 2011: 105-106 - 2010
- [j1]Gerwin Klein
seL4: formal verification of an operating-system kernel. Commun. ACM 53(6): 107-115 (2010) - [c6]David A. Cock:
Lyrebird - Assigning Meanings to Machines. SSV 2010
2000 – 2009
- 2009
- [c5]Gerwin Klein
seL4: formal verification of an OS kernel. SOSP 2009: 207-220 - [c4]Simon Winwood, Gerwin Klein
Mind the Gap. TPHOLs 2009: 500-515 - 2008
- [c3]David A. Cock:
Bitfields and Tagged Unions in C: Verification through Automatic Generation. VERIFY 2008 - [c2]David A. Cock
Secure Microkernels, State Monads and Scalable Refinement. TPHOLs 2008: 167-182 - 2006
- [c1]Philip Derrin, Kevin Elphinstone, Gerwin Klein, David A. Cock, Manuel M. T. Chakravarty:
Running the manual: an approach to high-assurance microkernel development. Haskell 2006: 60-71
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-03-05 20:52 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: