Abstraction, refinement and proof for probabilistic systems A McIver, CC Morgan Springer, 2004 | 445 | 2004 |

Probabilistic predicate transformers C Morgan, A McIver, K Seidel ACM Transactions on Programming Languages and Systems (TOPLAS) 18 (3), 325-353, 1996 | 346 | 1996 |

Probabilistic models for the guarded command language H Jifeng, K Seidel, A McIver Science of Computer Programming 28 (2-3), 171-192, 1997 | 188 | 1997 |

Refinement-oriented probability for CSP C Morgan, A McIver, K Seidel, JW Sanders Formal aspects of computing 8 (6), 617-647, 1996 | 111 | 1996 |

Probabilistic guarded commands mechanized in HOL J Hurd, A McIver, C Morgan Theoretical Computer Science 346 (1), 96-112, 2005 | 104 | 2005 |

Compositional closure for Bayes risk in probabilistic noninterference A McIver, L Meinicke, C Morgan International Colloquium on Automata, Languages, and Programming, 223-235, 2010 | 84 | 2010 |

Automated analysis of AODV using UPPAAL A Fehnker, R Van Glabbeek, P Höfner, A McIver, M Portmann, WL Tan International Conference on Tools and Algorithms for the Construction and …, 2012 | 82 | 2012 |

A process algebra for wireless mesh networks A Fehnker, R Van Glabbeek, P Höfner, A McIver, M Portmann, WL Tan European Symposium on Programming, 295-315, 2012 | 81 | 2012 |

pGCL: Formal reasoning for random algorithms C Morgan, A McI South African Computer Society (SAICSIT), 1999 | 79 | 1999 |

Linear-invariant generation for probabilistic programs JP Katoen, AK McIver, LA Meinicke, CC Morgan International Static Analysis Symposium, 390-406, 2010 | 77 | 2010 |

Additive and multiplicative notions of leakage, and their capacities MS Alvim, K Chatzikokolakis, A McIver, C Morgan, C Palamidessi, ... 2014 IEEE 27th Computer Security Foundations Symposium, 308-322, 2014 | 72 | 2014 |

Abstract channels and their robust information-leakage ordering A McIver, C Morgan, G Smith, B Espinoza, L Meinicke International Conference on Principles of Security and Trust, 83-102, 2014 | 63 | 2014 |

Partial correctness for probabilistic demonic programs AK McIver, C Morgan Theoretical Computer Science 266 (1-2), 513-541, 2001 | 58 | 2001 |

Enumerating finite groups A McIver, PM Neumann The Quarterly Journal of Mathematics 38 (4), 473-488, 1987 | 58 | 1987 |

A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV A Fehnker, R Van Glabbeek, P Höfner, A McIver, M Portmann, WL Tan arXiv preprint arXiv:1312.7645, 2013 | 57 | 2013 |

Operational versus weakest pre-expectation semantics for the probabilistic guarded command language F Gretz, JP Katoen, A McIver Performance Evaluation 73, 110-132, 2014 | 56 | 2014 |

Games, Probability, and the Quantitative μ-Calculus *qMμ*AK McIver, CC Morgan International Conference on Logic for Programming Artificial Intelligence …, 2002 | 55 | 2002 |

Results on the quantitative μ-calculus *qM*μA McIver, C Morgan ACM Transactions on Computational Logic (TOCL) 8 (1), 3-es, 2007 | 53 | 2007 |

A new proof rule for almost-sure termination A McIver, C Morgan, BL Kaminski, JP Katoen Proceedings of the ACM on Programming Languages 2 (POPL), 1-28, 2017 | 46 | 2017 |

A probabilistic temporal calculus based on expectations C Morgan, A McIver Proc. Formal Methods Pacific 97, 1997 | 43 | 1997 |