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 | 2029 | 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), 1-27, 2018 | 238 | 2018 |

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 | 89 | 2008 |

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 | 78 | 2014 |

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 | 54 | 2006 |

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 | 49 | 2009 |

Verifying probabilistic correctness in Isabelle with pGCL D Cock arXiv preprint arXiv:1211.6197, 2012 | 22 | 2012 |

Bitfields and Tagged Unions in C: Verification through Automatic Generation. D Cock VERIFY 8, 44-55, 2008 | 14 | 2008 |

Practical probability: Applying pGCL to lattice scheduling D Cock International Conference on Interactive Theorem Proving, 311-327, 2013 | 12 | 2013 |

Formalizing memory accesses and interrupts R Achermann, L Humbel, D Cock, T Roscoe arXiv preprint arXiv:1703.06571, 2017 | 11 | 2017 |

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 | 8 | 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 | 6 | 2017 |

pGCL for Isabelle D Cock Archive of Formal Proofs, 2014 | 6 | 2014 |

Leakage in Trustworthy Systems. D Cock University of New South Wales, Sydney, Australia, 2014 | 4 | 2014 |

Lyrebird-Assigning Meanings to Machines. D Cock SSV, 2010 | 3 | 2010 |

The Weyl algebras D Cock School of Mathematics, The University of New South Wales, 2004 | 3 | 2004 |

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 | 2 | 2019 |

From Operational Models to Information Theory; Side Channels in pGCL with Isabelle D Cock International Conference on Interactive Theorem Proving, 177-192, 2014 | 2 | 2014 |

Exploitation as an inference problem DA Cock Proceedings of the 4th ACM workshop on Security and artificial intelligence …, 2011 | 2 | 2011 |

Tackling Hardware/Software co-design from a database perspective. G Alonso, T Roscoe, D Cock, M Ewaida, K Kara, D Korolija, D Sidler, ... CIDR, 2020 | 1 | 2020 |