| 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 | 2871 | 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 | 527 | 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 | 124 | 2014 |
| Secure microkernels, state monads and scalable refinement D Cock, G Klein, T Sewell Theorem Proving in Higher Order Logics: 21st International Conference …, 2008 | 115 | 2008 |
| 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 | 67 | 2022 |
| 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 | 66 | 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 | 59 | 2006 |
| 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 | 28 | 2020 |
| Verifying probabilistic correctness in Isabelle with pGCL D Cock arXiv preprint arXiv:1211.6197, 2012 | 28 | 2012 |
| Formalizing memory accesses and interrupts R Achermann, L Humbel, D Cock, T Roscoe arXiv preprint arXiv:1703.06571, 2017 | 19 | 2017 |
| Bitfields and Tagged Unions in C: Verification through Automatic Generation. DA Cock VERIFY 8, 44-55, 2008 | 17 | 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 | 15 | 2018 |
| Practical probability: Applying pGCL to lattice scheduling D Cock International Conference on Interactive Theorem Proving, 311-327, 2013 | 15 | 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 | 10 | 2021 |
| pGCL for Isabelle D Cock Archive of Formal Proofs, 2014 | 8 | 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 | 7 | 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 | 7 | 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 | 7 | 2017 |
| 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 | 6 | 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 | 5 | 2021 |
Gernot HeiserProfessor of Computer Science, University of New South WalesVerified email at unsw.edu.au