Follow
David Cock
David Cock
Graduate Researcher, NICTA and University of New South Wales
Verified email at cse.unsw.edu.au - Homepage
Title
Cited by
Cited by
Year
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
23932009
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), 1-27, 2018
3652018
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
1032014
Secure microkernels, state monads and scalable refinement
D Cock, G Klein, T Sewell
International Conference on Theorem Proving in Higher Order Logics, 167-182, 2008
992008
Mind the gap
S Winwood, G Klein, T Sewell, J Andronick, D Cock, M Norrish
International Conference on Theorem Proving in Higher Order Logics, 500-515, 2009
592009
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
582006
Verifying probabilistic correctness in Isabelle with pGCL
D Cock
arXiv preprint arXiv:1211.6197, 2012
262012
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
182020
Formalizing memory accesses and interrupts
R Achermann, L Humbel, D Cock, T Roscoe
arXiv preprint arXiv:1703.06571, 2017
152017
Practical probability: Applying pGCL to lattice scheduling
D Cock
International Conference on Interactive Theorem Proving, 311-327, 2013
152013
Bitfields and Tagged Unions in C: Verification through Automatic Generation.
D Cock
VERIFY 8, 44-55, 2008
152008
Physical addressing on real hardware in Isabelle/HOL
R Achermann, L Humbel, D Cock, T Roscoe
International Conference on Interactive Theorem Proving, 1-19, 2018
112018
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
72017
pGCL for Isabelle
D Cock
Archive of Formal Proofs, 2014
72014
Leakage in Trustworthy Systems.
D Cock
University of New South Wales, Sydney, Australia, 2014
62014
The Enzian Coherent Interconnect (ECI): opening a coherence protocol to research and applications
A Ramdas, D Cock, T Roscoe, G Alonso
LATTE ˇ21, 2021
42021
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
32022
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
32021
A Model-Checked I2C Specification
L Humbel, D Schwyn, N Hossle, R Haecki, M Licciardello, J Schaer, ...
International Symposium on Model Checking Software, 177-193, 2021
32021
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
32019
The system can't perform the operation now. Try again later.
Articles 1–20