David Cock
David Cock
Senior Researcher, ETH Zurich
Verified email at - Homepage
Cited by
Cited by
seL4: Formal verification of an OS kernel
G Klein, K Elphinstone, G Heiser, J Andronick, D Cock, P Derrin, ...
Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles …, 2009
A survey of microarchitectural timing attacks and countermeasures on contemporary hardware
Q Ge, Y Yarom, D Cock, G Heiser
Journal of Cryptographic Engineering 8, 1-27, 2018
The last mile: An empirical study of timing channels on seL4
D Cock, Q Ge, T Murray, G Heiser
Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications …, 2014
Secure microkernels, state monads and scalable refinement
D Cock, G Klein, T Sewell
Theorem Proving in Higher Order Logics: 21st International Conference …, 2008
Mind the gap: A verification framework for low-level C
S Winwood, G Klein, T Sewell, J Andronick, D Cock, M Norrish
Theorem Proving in Higher Order Logics: 22nd International Conference …, 2009
Running the manual: An approach to high-assurance microkernel development
P Derrin, K Elphinstone, G Klein, D Cock, MMT Chakravarty
Proceedings of the 2006 ACM SIGPLAN workshop on Haskell, 60-71, 2006
Enzian: an open, general, CPU/FPGA platform for systems software research
D Cock, A Ramdas, D Schwyn, M Giardino, A Turowski, Z He, N Hossle, ...
Proceedings of the 27th ACM International Conference on Architectural …, 2022
Tackling Hardware/Software co-design from a database perspective
G Alonso, T Roscoe, D Cock, M Ewaida, K Kara, D Korolija, D Sidler, ...
10th Annual Conference on Innovative Data Systems Research (CIDR 2020 …, 2020
Verifying probabilistic correctness in Isabelle with pGCL
D Cock
arXiv preprint arXiv:1211.6197, 2012
Formalizing memory accesses and interrupts
R Achermann, L Humbel, D Cock, T Roscoe
arXiv preprint arXiv:1703.06571, 2017
Bitfields and Tagged Unions in C: Verification through Automatic Generation.
DA Cock
VERIFY 8, 44-55, 2008
Physical addressing on real hardware in Isabelle/HOL
R Achermann, L Humbel, D Cock, T Roscoe
Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as …, 2018
Practical probability: Applying pGCL to lattice scheduling
D Cock
International Conference on Interactive Theorem Proving, 311-327, 2013
A Model-Checked I2C Specification
L Humbel, D Schwyn, N Hossle, R Haecki, M Licciardello, J Schaer, ...
Model Checking Software: 27th International Symposium, SPIN 2021, Virtual …, 2021
Towards correct-by-construction interrupt routing on real hardware
L Humbel, R Achermann, D Cock, T Roscoe
Proceedings of the 9th Workshop on Programming Languages and Operating …, 2017
pGCL for Isabelle
D Cock
Archive of Formal Proofs, 2014
Declarative power sequencing
J Schult, D Schwyn, M Giardino, D Cock, R Achermann, T Roscoe
ACM Transactions on Embedded Computing Systems (TECS) 20 (5s), 1-21, 2021
The Enzian Coherent Interconnect (ECI): opening a coherence protocol to research and applications
A Ramdas, D Cock, T Roscoe, G Alonso
LATTE ‘21, 2021
CleanQ: a lightweight, uniform, formally specified interface for intra-machine data transfer
R Haecki, L Humbel, R Achermann, D Cock, D Schwyn, T Roscoe
arXiv preprint arXiv:1911.08773, 2019
mmapx: Uniform memory protection in a heterogeneous world
R Achermann, D Cock, R Haecki, N Hossle, L Humbel, T Roscoe, ...
Proceedings of the Workshop on Hot Topics in Operating Systems, 159-166, 2021
The system can't perform the operation now. Try again later.
Articles 1–20