| 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 | 2538 | 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 | 405 | 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 | 109 | 2014 |
| Secure microkernels, state monads and scalable refinement D Cock, G Klein, T Sewell Theorem Proving in Higher Order Logics: 21st International Conference …, 2008 | 108 | 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 | 63 | 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 | 58 | 2006 |
| Verifying probabilistic correctness in Isabelle with pGCL D Cock arXiv preprint arXiv:1211.6197, 2012 | 25 | 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 | 23 | 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 | 18 | 2022 |
| Formalizing memory accesses and interrupts R Achermann, L Humbel, D Cock, T Roscoe arXiv preprint arXiv:1703.06571, 2017 | 16 | 2017 |
| Practical probability: Applying pGCL to lattice scheduling D Cock Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes …, 2013 | 15 | 2013 |
| Bitfields and Tagged Unions in C: Verification through Automatic Generation. D Cock VERIFY 8, 44-55, 2008 | 15 | 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 | 11 | 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 | 8 | 2017 |
| pGCL for Isabelle D Cock Archive of Formal Proofs, 2014 | 7 | 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 | 5 | 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 | 5 | 2021 |
| Leakage in Trustworthy Systems. D Cock University of New South Wales, Sydney, Australia, 2014 | 5 | 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 | 4 | 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 | 3 | 2019 |
