David Cock
David Cock
Graduate Researcher, NICTA and University of New South Wales
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
Verifying probabilistic correctness in Isabelle with pGCL
D Cock
arXiv preprint arXiv:1211.6197, 2012
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
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
Formalizing memory accesses and interrupts
R Achermann, L Humbel, D Cock, T Roscoe
arXiv preprint arXiv:1703.06571, 2017
Practical probability: Applying pGCL to lattice scheduling
D Cock
Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes …, 2013
Bitfields and Tagged Unions in C: Verification through Automatic Generation.
D 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
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
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
Leakage in Trustworthy Systems.
D Cock
University of New South Wales, Sydney, Australia, 2014
The Enzian Coherent Interconnect (ECI): opening a coherence protocol to research and applications
A Ramdas, D Cock, T Roscoe, G Alonso
LATTE ‘21, 2021
A least-privilege memory protection model for modern hardware
R Achermann, N Hossle, L Humbel, D Schwyn, D Cock, T Roscoe
arXiv preprint arXiv:1908.08707, 2019
The system can't perform the operation now. Try again later.
Articles 1–20