Back to
Professor Carroll Morgan
Professor

Professor Carroll Morgan

Engineering
Computer Science and Engineering

Professor Carroll Morgan is professor in the School of Computer Science and Engineering. His research interests include formal specification and program development by refinement, probabilistic semantics, concurrency and quantitative information flow (cyber security).

He studied at UNSW (BSc) and Sydney University (PhD), and was at Oxford University from 1982-99. Since 2000 he has been with UNSW and (now called) Trustworthy Systems jointly.
E-mail
carroll.morgan@unsw.edu.au
Location
School of Computer Science and Engineering Computer Science Building K17 UNSW Kensington Campus Sydney NSW 2052
  • Books | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, The Science of Quantitative Information Flow, Springer International Publishing, http://dx.doi.org/10.1007/978-3-319-96131-6
    Books | 2009
    Leucker M; Morgan C, 2009, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface
    Books | 2005
    Morgan CC; McIver A, 2005, Abstraction, refinement and proof for probabilistic systems, 1, Springer Verlag, New York, http://portal.acm.org/citation.cfm?id=1036296
    Books | 2003
    2003, Programming Methodology, Morgan CC; McIver A, (ed.), Springer Publishing Company, New York, http://www.springer.com/computer/swe/book/978-0-387-95349-6
  • Book Chapters | 2021
    Bird R; Gibbons J; Hinze R; Höfner P; Jeuring J; Meertens L; Möller B; Morgan C; Schrijvers T; Swierstra W; Wu N, 2021, 'Algorithmics', in Advancing Research in Information and Communication Technology, Springer International Publishing, pp. 59 - 98, http://dx.doi.org/10.1007/978-3-030-81701-5_3
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'A demonic lattice of information', in Information Security and Cryptography, pp. 325 - 350, http://dx.doi.org/10.1007/978-3-319-96131-6_17
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'Axiomatics', in Information Security and Cryptography, pp. 183 - 204, http://dx.doi.org/10.1007/978-3-319-96131-6_11
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'Capacity', in Information Security and Cryptography, pp. 107 - 130, http://dx.doi.org/10.1007/978-3-319-96131-6_7
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'Channels', in Information Security and Cryptography, pp. 49 - 70, http://dx.doi.org/10.1007/978-3-319-96131-6_4
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'Composition of channels', in Information Security and Cryptography, pp. 131 - 145, http://dx.doi.org/10.1007/978-3-319-96131-6_8
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'Defense against side channels', in Information Security and Cryptography, pp. 389 - 397, http://dx.doi.org/10.1007/978-3-319-96131-6_20
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'Differential privacy', in Information Security and Cryptography, pp. 433 - 444, http://dx.doi.org/10.1007/978-3-319-96131-6_23
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'Hidden-Markov modeling of QIF in sequential programs', in Information Security and Cryptography, pp. 255 - 282, http://dx.doi.org/10.1007/978-3-319-96131-6_14
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'Introduction', in Information Security and Cryptography, pp. 3 - 13, http://dx.doi.org/10.1007/978-3-319-96131-6_1
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'Iteration and nontermination', in Information Security and Cryptography, pp. 307 - 323, http://dx.doi.org/10.1007/978-3-319-96131-6_16
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'Modeling secrets', in Information Security and Cryptography, pp. 17 - 23, http://dx.doi.org/10.1007/978-3-319-96131-6_2
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'Multi-party computation: The Three Judges protocol', in Information Security and Cryptography, pp. 399 - 411, http://dx.doi.org/10.1007/978-3-319-96131-6_21
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'On $$ \mathit {g} $$ -vulnerability', in Information Security and Cryptography, pp. 25 - 46, http://dx.doi.org/10.1007/978-3-319-96131-6_3
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'Posterior vulnerability and leakage', in Information Security and Cryptography, pp. 71 - 100, http://dx.doi.org/10.1007/978-3-319-96131-6_5
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'Program algebra for QIF', in Information Security and Cryptography, pp. 283 - 305, http://dx.doi.org/10.1007/978-3-319-96131-6_15
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'Quantitative information flow in sequential computer programs', in Information Security and Cryptography, pp. 225 - 253, http://dx.doi.org/10.1007/978-3-319-96131-6_13
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'Refinement', in Information Security and Cryptography, pp. 147 - 170, http://dx.doi.org/10.1007/978-3-319-96131-6_9
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'Robustness', in Information Security and Cryptography, pp. 101 - 105, http://dx.doi.org/10.1007/978-3-319-96131-6_6
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'The Crowds protocol', in Information Security and Cryptography, pp. 353 - 367, http://dx.doi.org/10.1007/978-3-319-96131-6_18
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'The Dalenius perspective', in Information Security and Cryptography, pp. 171 - 181, http://dx.doi.org/10.1007/978-3-319-96131-6_10
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'The geometry of hypers, gains and losses', in Information Security and Cryptography, pp. 205 - 221, http://dx.doi.org/10.1007/978-3-319-96131-6_12
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'Timing attacks on blinded and bucketed cryptography', in Information Security and Cryptography, pp. 369 - 388, http://dx.doi.org/10.1007/978-3-319-96131-6_19
    Book Chapters | 2020
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2020, 'Voting systems', in Information Security and Cryptography, pp. 413 - 431, http://dx.doi.org/10.1007/978-3-319-96131-6_22
    Book Chapters | 2020
    Gibbons J; McIver A; Morgan C; Schrijvers T, 2020, 'Quantitative Information Flow with Monads in Haskell', in Foundations of Probabilistic Programming, Cambridge University Press, pp. 391 - 448, http://dx.doi.org/10.1017/9781108770750.013
    Book Chapters | 2019
    Rabehaja T; McIver A; Morgan C; Struth G, 2019, 'Categorical Information Flow', in The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy, pp. 329 - 343, http://dx.doi.org/10.1007/978-3-030-31175-9_19
    Book Chapters | 2017
    Morgan C, 2017, 'A demonic lattice of information', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer, Cham, pp. 203 - 222, http://dx.doi.org/10.1007/978-3-319-51046-0_11
    Book Chapters | 2010
    McIver A; Morgan CC, 2010, 'The thousand-and-one cryptographers', in Wood K; Roscoe AW; Jones CB (ed.), Reflections on the work of C.A.R. Hoare, Springer, New York, pp. 255 - 282, http://dx.doi.org/10.1007/978-1-84882-912-1_12
    Book Chapters | 2006
    Morgan CC; McIver A, 2006, 'Developing and Reasoning about probabilistic programs in pGCL', in Cavalcanti ; Sampaio ; Woodcock (ed.), Refinement Techniques in Software Engineering, Springer Publishing Company, Germany, pp. 123 - 155
    Book Chapters | 2006
    Morgan CC; McIver A, 2006, 'Programming-Logic Analysis of Fault Tolerance', in Butler ; Jones ; Romanovsky ; Troubitsyna (ed.), Rigorous Development of Complex Fault-Tolerant Systems, edn. First, Springer Publishing Company, Germany, pp. 288 - 305
    Book Chapters | 2005
    Hoang TS; Jin Z; Robinson K; McIver A; Morgan C, 2005, 'Development via Refinement in Probabilistic B — Foundation and Case Study', in ZB 2005: Formal Specification and Development in Z and B, Springer Berlin Heidelberg, pp. 355 - 373, http://dx.doi.org/10.1007/11415787_21
    Book Chapters | 2005
    Morgan CC, 2005, 'Of probabilistic wp and CSP - and compositionality', in Abdallah ; Jones ; Roscoe ; Sanders (ed.), Proceedings of the First International Conference on Advances in Natural Computation (ICNC 2005), Part III, Lecture Notes in Computer Science 3612/2005, Springer, Berlin, Germany, pp. 220 - 241
    Book Chapters | 2003
    Morgan CC; McIver A, 2003, 'A probabilistic approach to information hiding', in Morgan C; McIver A (ed.), Programming Methodology, edn. 1, Springer Publishing Company, New York, pp. 441 - 460, http://portal.acm.org/citation.cfm?id=766972
    Book Chapters | 1993
    Morgan C, 1993, 'The refinement calculus, and literate development', in Formal Program Development, Springer Berlin Heidelberg, pp. 161 - 182, http://dx.doi.org/10.1007/3-540-57499-9_20
    Book Chapters | 1992
    Hoare CAR; Hayes IJ; Jifeng H; Morgan CC; Roscoe AW; Sanders JW; Sorenson IH; Spivey JM; Sufrin BA, 1992, 'Laws of Programming', in Programming and Mathematical Method, Springer Berlin Heidelberg, pp. 95 - 122, http://dx.doi.org/10.1007/978-3-642-77572-7_7
    Book Chapters | 1990
    Morgan C, 1990, 'Of wp and CSP', in Beauty Is Our Business, Springer New York, pp. 319 - 326, http://dx.doi.org/10.1007/978-1-4612-4476-9_37
  • Journal articles | 2022
    Alvim MS; Fernandes N; McIver A; Morgan C; Nunes GH, 2022, 'Flexible and scalable privacy assessment for very large datasets, with an application to official governmental microdata', Proceedings on Privacy Enhancing Technologies, 2022, pp. 378 - 399, http://dx.doi.org/10.56553/popets-2022-0114
    Journal articles | 2021
    Fernandes N; McIver A; Morgan C, 2021, 'The Laplace Mechanism has optimal utility for differential privacy over continuous queries', Proceedings - Symposium on Logic in Computer Science, 2021-June, http://dx.doi.org/10.1109/LICS52264.2021.9470718
    Journal articles | 2020
    Höfner P; Morgan C; Pratt V, 2020, 'Preface', Acta Informatica, 57, pp. 305 - 311, http://dx.doi.org/10.1007/s00236-020-00382-7
    Journal articles | 2019
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2019, 'An axiomatization of information flow measures', Theoretical Computer Science, 777, pp. 32 - 54, http://dx.doi.org/10.1016/j.tcs.2018.10.016
    Journal articles | 2019
    Mc Iver A; Morgan C; Rabehaja T, 2019, 'Abstract hidden markov models: A monadic account of quantitative information flow', Logical Methods in Computer Science, 15, pp. 36:1-36:50, http://dx.doi.org/10.23638/LMCS-15(1:36)2019
    Journal articles | 2019
    McIver AK; Morgan CC; Rabehaja T, 2019, 'Program algebra for quantitative information flow', Journal of Logical and Algebraic Methods in Programming, 106, pp. 55 - 77, http://dx.doi.org/10.1016/j.jlamp.2019.04.002
    Journal articles | 2018
    McIver A; Morgan C; Kaminski BL; Katoen JP, 2018, 'A new proof rule for almost-sure termination', Proceedings of the ACM on Programming Languages, 2, pp. 1 - 28, http://dx.doi.org/10.1145/3158121
    Journal articles | 2017
    McIver A; Rabehaja T; Wen R; Morgan C, 2017, 'Privacy in elections: How small is “small”?', Journal of Information Security and Applications, 36, pp. 112 - 126, http://dx.doi.org/10.1016/j.jisa.2017.08.003
    Journal articles | 2014
    Deng Y; van Glabbeek R; Hennessy M; Morgan C, 2014, 'Real-reward testing for probabilistic processes', Theoretical Computer Science, 538, pp. 16 - 36, http://dx.doi.org/10.1016/j.tcs.2013.07.016
    Journal articles | 2014
    Hoang TS; McIver AK; Meinicke L; Morgan CC; Sloane A; Susatyo E, 2014, 'Abstractions of non-interference security: Probabilistic versus possibilistic', Formal Aspects of Computing, 26, pp. 169 - 194, http://dx.doi.org/10.1007/s00165-012-0237-4
    Journal articles | 2014
    Mciver A; Meinicke L; Morgan C, 2014, 'Hidden-Markov program algebra with iteration', Mathematical Structures in Computer Science, 29, http://dx.doi.org/10.1017/S0960129513000625
    Journal articles | 2014
    Morgan C, 2014, 'An old new notation for elementary probability theory', Science of Computer Programming, 85, pp. 115 - 136, http://dx.doi.org/10.1016/j.scico.2013.09.003
    Journal articles | 2014
    Simao A; Morgan C, 2014, 'Selected papers from the Brazilian Symposium on Formal Methods (SBMF 2011)', Science of Computer Programming, 92, pp. 85, http://dx.doi.org/10.1016/j.scico.2014.02.004
    Journal articles | 2013
    Morgan CC, 2013, 'Lattices of information for security: Deterministic, demonic, probabilistic', Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8144 LNCS, pp. 1 - 3, http://dx.doi.org/10.1007/978-3-642-41202-8_1
    Journal articles | 2012
    Hoang TS; McIver AK; Meinicke L; Sloane A; Susatyo E; Morgan CC, 2012, 'Abstractions of non-interference security: probabilistic versus possibilistic', Formal Aspects of Computing, pp. 1 - 26, http://dx.doi.org/10.1007/s00165-012-0237-4
    Journal articles | 2012
    Morgan CC, 2012, 'Compositional noninterference from first principles', Formal Aspects of Computing, 24, pp. 3 - 26, http://dx.doi.org/10.1007/s00165-010-0167-y
    Journal articles | 2012
    Morgan CC, 2012, 'Compositional noninterference from first principles', Formal Aspects of Computing, 24, pp. 3 - 26, http://dx.doi.org/10.1007/s00165-010-0167-y
    Journal articles | 2010
    McIver A; Morgan CC, 2010, 'Compositional refinement in agent-based security protocols', Formal Aspects of Computing, 23, pp. 711 - 737, http://dx.doi.org/10.1007/s00165-010-0164-1
    Journal articles | 2009
    Morgan CC, 2009, 'The Shadow Knows: Refinement and security in sequential programs', Science of Computer Programming, 74, pp. 629 - 653, http://dx.doi.org/10.1016/j.scico.2007.09.003
    Journal articles | 2008
    Deng Y; van Glabbeek RJ; Hennessy M; Morgan CC, 2008, 'Characterising Testing Preorders for Finite Probabilistic Processes', Logical Methods in Computer Science, 4, http://dx.doi.org/10.2168/LMCS-4(4:4)2008
    Journal articles | 2008
    McIver A; Gonzalia C; Cohen EG; Morgan CC, 2008, 'Using probabilistic Kleene algebra pKA for protocol verification', Journal of Logic and Algebraic Programming, 76, pp. 90 - 111, http://dx.doi.org/10.1016/j.jlap.2007.10.005
    Journal articles | 2007
    Deng Y; van Glabbeek RJ; Hennessy M; Morgan CC; Zhang C, 2007, 'Remarks on Testing Probabilistic Processes', Electronic Notes in Theoretical Computer Science, 172, pp. 359 - 397, http://dx.doi.org/10.1016/j.entcs.2007.02.013
    Journal articles | 2007
    McIver A; Morgan CC, 2007, 'Results on the quantitative mu-calculus qM mu', ACM Transactions on Computational Logic, 8, pp. 3:1 - 3:43, http://dx.doi.org/10.1145/1182613.1182616
    Journal articles | 2006
    Morgan C, 2006, 'The shadow knows: Refinement of ignorance in sequential programs', Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 4014 LNCS, pp. 359 - 378, http://dx.doi.org/10.1007/11783596_21
    Journal articles | 2005
    McIver A; Morgan CC, 2005, 'An elementary proof that Herman`s Ring is Theta (N-2)', Information Processing Letters, 94, pp. 79 - 84, http://dx.doi.org/10.1016/j.ipl.2004.12.013
    Journal articles | 2005
    Morgan CC; Hoang TS; Abrial J, 2005, 'The challenge of probabilistic Event B - Extended abstract', 13th International Conference on FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FoSSaCS 2010), 3455, pp. 162 - 171, http://dx.doi.org/10.1007/11415787_10
    Journal articles | 2005
    Morgan CC; McIver A; Hurd J, 2005, 'Abstraction and refinement in probabilistic systems', ACM SIGMETRICS performance evaluation review, 346, pp. 41 - 47, http://dx.doi.org/10.1145/1059816.1059824
    Journal articles | 2005
    Morgan CC; McIver A; Hurd J, 2005, 'Probabilistic guarded commands mechanised in HOL', Theoretical Computer Science, 346, pp. 96 - 112, http://dx.doi.org/10.1016/j.tcs.2005.08.005
    Journal articles | 2003
    Morgan CC; McIver A, 2003, 'Almost-certain eventualities and abstract probabilities in quantitative temporal logic', Theoretical Computer Science, 293, pp. 507 - 534, http://dx.doi.org/10.1016/S0304-3975(02)00612-6
    Journal articles | 2001
    McIver A; Morgan C, 2001, 'Almost-certain eventualities and abstract probabilities in quantitative temporal logic', Electronic Notes in Theoretical Computer Science, 42, pp. 12 - 40, http://dx.doi.org/10.1016/S1571-0661(04)80876-4
    Journal articles | 2001
    McIver AK; Morgan C, 2001, 'Demonic, angelic and unbounded probabilistic choices in sequential programs', Acta Informatica, 37, pp. 329 - 354, http://dx.doi.org/10.1007/s002360000046
    Journal articles | 2001
    McIver AK; Morgan C, 2001, 'Partial correctness for probabilistic demonic programs', Theoretical Computer Science, 266, pp. 513 - 541, http://dx.doi.org/10.1016/S0304-3975(00)00208-5
    Journal articles | 2001
    Morgan C; McIver A, 2001, 'Cost analysis of games, using program logic', Proceedings of the Asia-Pacific Software Engineering Conference and International Computer Science Conference, APSEC and ICSC, pp. 351
    Journal articles | 1998
    Alvord L; Court J; Davis T; Morgan CC; Schindhelm KH; Vogt J; Winterton LW, 1998, 'The oxygen permeability of a new type of high Dk soft contact lens material', Optometry and Vision Science, 75, pp. 30 - 36, http://dx.doi.org/10.1097/00006324-199801000-00022
    Journal articles | 1997
    Seidel K; Morgan C, 1997, 'Hierarchical Reasoning in Probabilistic CSP', Programming and Computer Software, 23, pp. 239 - 250
    Journal articles | 1996
    Morgan C; McIver A; Seidel K; Sanders JW, 1996, 'Refinement-oriented probability for CSP', Formal Aspects of Computing, 8, pp. 617 - 647, http://dx.doi.org/10.1007/BF01213492
    Journal articles | 1996
    Morgan C; McIver A; Seidel K, 1996, 'Probabilistic Predicate Transformers', ACM Transactions on Programming Languages and Systems, 18, pp. 325 - 353, http://dx.doi.org/10.1145/229542.229547
    Journal articles | 1996
    Morgan C; McIver A, 1996, 'Unifying wp and wlp', Information Processing Letters, 59, pp. 159 - 163, http://dx.doi.org/10.1016/0020-0190(96)00093-2
    Journal articles | 1995
    Butler M; Morgan C, 1995, 'Action systems, unbounded nondeterminism, and infinite traces', Formal Aspects of Computing, 7, pp. 37 - 53, http://dx.doi.org/10.1007/BF01214622
    Journal articles | 1995
    King S; Morgan C, 1995, 'Exits in the refinement calculus', Formal Aspects of Computing, 7, pp. 54 - 76, http://dx.doi.org/10.1007/BF01214623
    Journal articles | 1993
    Gardiner PHB; Morgan C, 1993, 'A single complete rule for data refinement', Formal Aspects of Computing, 5, pp. 367 - 382, http://dx.doi.org/10.1007/BF01212407
    Journal articles | 1991
    Gardiner P; Morgan C, 1991, 'Data refinement of predicate transformers', Theoretical Computer Science, 87, pp. 143 - 162, http://dx.doi.org/10.1016/0304-3975(91)90029-2
    Journal articles | 1990
    Morgan C; Gardiner PHB, 1990, 'Data refinement by calculation', Acta Informatica, 27, pp. 481 - 503, http://dx.doi.org/10.1007/BF00277386
    Journal articles | 1990
    Morgan C; Vickers T, 1990, 'Types and invariants in the refinement calculus', Science of Computer Programming, 14, pp. 281 - 304, http://dx.doi.org/10.1016/0167-6423(90)90024-8
    Journal articles | 1988
    Morgan C, 1988, 'Auxiliary variables in data refinement', Information Processing Letters, 29, pp. 293 - 296, http://dx.doi.org/10.1016/0020-0190(88)90227-X
    Journal articles | 1988
    Morgan C, 1988, 'Procedures, parameters, and abstraction: Separate concerns', Science of Computer Programming, 11, pp. 17 - 27, http://dx.doi.org/10.1016/0167-6423(88)90062-7
    Journal articles | 1988
    Morgan C, 1988, 'The Specification Statement', ACM Transactions on Programming Languages and Systems (TOPLAS), 10, pp. 403 - 419, http://dx.doi.org/10.1145/44501.44503
    Journal articles | 1988
    Morgan CC, 1988, 'Data refinement by miracles', Information Processing Letters, 26, pp. 243 - 246, http://dx.doi.org/10.1016/0020-0190(88)90147-0
    Journal articles | 1987
    Hoare CAR; Hayes IJ; Jifeng H; Morgan CC; Roscoe AW; Sanders JW; Sorensen IH; Spivey JM; Sufrin BA, 1987, 'Laws of programming', Communications of the ACM, 30, pp. 672 - 686, http://dx.doi.org/10.1145/27651.27653
    Journal articles | 1987
    Morgan C; Robinson K, 1987, 'SPECIFICATION STATEMENTS AND REFINEMENT.', IBM Journal of Research and Development, 31, pp. 546 - 555, http://dx.doi.org/10.1147/rd.315.0546
    Journal articles | 1985
    Morgan C, 1985, 'Global and logical time in distributed algorithms', Information Processing Letters, 20, pp. 189 - 194, http://dx.doi.org/10.1016/0020-0190(85)90048-1
    Journal articles | 1984
    Morgan C; Sufrin B, 1984, 'Specification of the UNIX Filing System', IEEE Transactions on Software Engineering, SE-10, pp. 128 - 142, http://dx.doi.org/10.1109/TSE.1984.5010215
  • Preprints | 2023
    Alvim MS; Fernandes N; McIver A; Morgan C; Nunes GH, 2023, A novel analysis of utility in privacy pipelines, using Kronecker products and quantitative information flow, , http://dx.doi.org/10.48550/arxiv.2308.11110
    Preprints | 2022
    Alvim MS; Fernandes N; McIver A; Morgan C; Nunes GH, 2022, Flexible and scalable privacy assessment for very large datasets, with an application to official governmental microdata, , http://dx.doi.org/10.48550/arxiv.2204.13734
    Conference Papers | 2022
    Fernandes N; McIver A; Morgan C, 2022, 'How to Develop an Intuition for Risk. . . and Other Invisible Phenomena', in Leibniz International Proceedings in Informatics, LIPIcs, http://dx.doi.org/10.4230/LIPIcs.CSL.2022.2
    Preprints | 2021
    Fernandes N; McIver A; Morgan C, 2021, The Laplace Mechanism has optimal utility for differential privacy over continuous queries, , http://dx.doi.org/10.48550/arxiv.2105.07176
    Conference Papers | 2020
    McIver A; Morgan C, 2020, 'Correctness by Construction for Probabilistic Programs', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 216 - 239, http://dx.doi.org/10.1007/978-3-030-61362-4_12
    Conference Papers | 2019
    McIver A; Morgan C, 2019, 'Proving that programs are differentially private', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bali, Indonesia, pp. 3 - 18, presented at 17th Asian symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Bali, Indonesia, 01 December 2019 - 04 December 2019, http://dx.doi.org/10.1007/978-3-030-34175-6_1
    Conference Papers | 2017
    Bordenabe N; McIver A; Morgan C; Rabehaja T, 2017, 'Reasoning about distributed secrets', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Neuchâtel, Switzerland, pp. 156 - 170, presented at 37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, 19 June 2017 - 22 June 2017, http://dx.doi.org/10.1007/978-3-319-60225-7_11
    Preprints | 2017
    McIver A; Morgan C; Kaminski BL; Katoen J-P, 2017, A New Proof Rule for Almost-Sure Termination, , http://dx.doi.org/10.48550/arxiv.1711.03588
    Preprints | 2017
    McIver A; Morgan C; Rabehaja T, 2017, Abstract Hidden Markov Models: a monadic account of quantitative information flow, , http://dx.doi.org/10.48550/arxiv.1708.01688
    Conference Papers | 2017
    McIver AK; Morgan CC; Rabehaja T, 2017, 'Algebra for quantitative information flow', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Lyon, France, pp. 3 - 23, presented at 16th International Conference, RAMiCS 2017, Lyon, France, 15 May 2017 - 18 May 2017, http://dx.doi.org/10.1007/978-3-319-57418-9_1
    Conference Papers | 2016
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2016, 'Axioms for information leakage', in Proceedings - IEEE Computer Security Foundations Symposium, Lisbon, Portugal, presented at 2016 IEEE 29th Computer Security Foundations Symposium (CSF), Lisbon, Portugal, 27 June 2016 - 01 July 2016, http://dx.doi.org/10.1109/CSF.2016.13
    Conference Papers | 2016
    Andronick J; Lewis C; Matichuk D; Morgan C; Rizkallah C, 2016, 'Proof of OS scheduling behavior in the presence of interrupt-induced concurrency', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Nancy, France, pp. 52 - 68, presented at International Conference on Interactive Theorem Proving 2016, Nancy, France, 22 August 2016 - 27 August 2016, http://dx.doi.org/10.1007/978-3-319-43144-4_4
    Preprints | 2016
    Bordenabe N; McIver A; Morgan C; Rabehaja T, 2016, Compositional security and collateral leakage, , http://dx.doi.org/10.48550/arxiv.1604.04983
    Conference Papers | 2015
    Andronick J; Lewis C; Morgan C, 2015, 'Controlled owicki-gries concurrency: Reasoning about the preemptible eChronos embedded operating system', in Electronic Proceedings in Theoretical Computer Science, EPTCS, pp. 10 - 24, http://dx.doi.org/10.4204/EPTCS.196.2
    Preprints | 2015
    Andronick J; Lewis C; Morgan C, 2015, Controlled Owicki-Gries Concurrency: Reasoning about the Preemptible eChronos Embedded Operating System, , http://dx.doi.org/10.48550/arxiv.1511.04170
    Conference Papers | 2015
    McIver A; Morgan C; Rabehaja T, 2015, 'Abstract hidden markov models: A monadic account of quantitative information flow', in Proceedings - Symposium on Logic in Computer Science, pp. 597 - 608, http://dx.doi.org/10.1109/LICS.2015.61
    Conference Papers | 2015
    Morgan C, 2015, 'A nondeterministic lattice of information', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 9 - 10
    Conference Papers | 2014
    Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2014, 'Additive and multiplicative notions of leakage, and their capacities', in Proceedings of the Computer Security Foundations Workshop, pp. 308 - 322, http://dx.doi.org/10.1109/CSF.2014.29
    Conference Papers | 2014
    McIver A; Morgan C; Smith G; Espinoza B; Meinicke L, 2014, 'Abstract channels and their robust information-leakage ordering', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 83 - 102, http://dx.doi.org/10.1007/978-3-642-54792-8_5
    Conference Papers | 2014
    Morgan C, 2014, '(In-)formal methods: The lost art a users’ manual', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Chongqing, China, pp. 1 - 79, presented at First International School, SETSS 2014, Chongqing, China, 08 September 2014 - 13 September 2014, http://dx.doi.org/10.1007/978-3-319-29628-9_1
    Conference Papers | 2014
    Wen R; McIver A; Morgan C, 2014, 'Towards a formal analysis of information leakage for signature attacks in preferential elections', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 595 - 610, http://dx.doi.org/10.1007/978-3-319-06410-9_40
    Conference Papers | 2012
    McIver A; Meinicke L; Morgan CC, 2012, 'A Kantorovich-monadic powerdomain for information hiding, with probability and nondeterminism', in Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, New Jersey, pp. 461 - 470, presented at Logic in Computer Science, Dubrovnik, http://dx.doi.org/10.1109/LICS.2012.56
    Conference Papers | 2012
    Morgan CC, 2012, 'Elementary probability theory in the Eindhoven style', in 11th International Conference, MPC 2012, Springer, Heidelberg, pp. 48 - 73, presented at Maths of Program Construction, Madrid, 25 June 2012, http://dx.doi.org/10.1007/978-3-642-31113-0_5
    Preprints | 2011
    Deng Y; van Glabbeek R; Hennessy M; Morgan C, 2011, Real-Reward Testing for Probabilistic Processes (Extended Abstract), , http://dx.doi.org/10.48550/arxiv.1107.1201
    Preprints | 2011
    McIver A; Meinicke L; Morgan C, 2011, Hidden-Markov Program Algebra with iteration, , http://dx.doi.org/10.48550/arxiv.1102.0333
    Conference Papers | 2010
    Katoen J-P; McIver AK; Meinicke LA; Morgan CC, 2010, 'Linear-Invariant Generation for Probabilistic Programs: Automated Support for Proof-Based Methods', in Cousot R; Martel M (ed.), STATIC ANALYSIS, SPRINGER, FRANCE, Perpignan, pp. 390 - +, presented at 17th International Static Analysis Symposium, FRANCE, Perpignan, 14 September 2010 - 16 September 2010, https://www.webofscience.com/api/gateway?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:000286149800024&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=891bb5ab6ba270e68a29b250adbe88d1
    Conference Papers | 2010
    Katoen J; McIver A; Meinicke L; Morgan CC, 2010, 'Linear-invariant generation for probabilistic programs', in AICI - Lecture Notes in Computer Science, Springer, Germany, pp. 390 - 406, presented at SAS 2010, Perpingnan, http://dx.doi.org/10.1007/978-3-642-15769-1_24
    Conference Papers | 2010
    McIver A; Meinicke L; Morgan C, 2010, 'Compositional closure for bayes risk in probabilistic noninterference', in Abramsky S; Gavoille C; Kirchner C; MeyerAufDerHeide F; Spirakis PG (eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), SPRINGER-VERLAG BERLIN, Bordeaux, FRANCE, pp. 223 - 235, presented at 37th International Colloquium on Automata, Languages and Programming, Bordeaux, FRANCE, 06 July 2010 - 10 July 2010, http://dx.doi.org/10.1007/978-3-642-14162-1_19
    Preprints | 2010
    McIver A; Meinicke L; Morgan C, 2010, Compositional closure for Bayes Risk in probabilistic noninterference, , http://dx.doi.org/10.48550/arxiv.1007.1054
    Conference Papers | 2010
    McIver A; Meinicke L; Morgan CC, 2010, 'Compositional closure for Bayes Risk in sequential noninterference', in Proceedings ICALP 2010, LNCS 6199, Springer, Bordeaux, pp. 223 - 235, presented at ICALP 2010, Bordeaux, http://portal.acm.org/citation.cfm?id=1880999.1881023
    Conference Papers | 2009
    Andova S; D'Argenio P; Cuijpers P; McIver A; Markovski J; Morgan C; Núñez M, 2009, 'Preface', in Electronic Proceedings in Theoretical Computer Science, EPTCS, http://dx.doi.org/10.4204/EPTCS.13
    Conference Papers | 2009
    Deng Y; Hennessy M; van Glabbeek RJ; Morgan CC, 2009, 'Testing Finitary Probabilistic Processes', in Proceedings of the First International Conference on Advances in Natural Computation (ICNC 2005), Part III, Lecture Notes in Computer Science 3612/2005, Springer, Berlin, Germany, pp. 274 - 288, presented at 20th International Conference on Concurrency Theory, Bologna, Italy, http://dx.doi.org/10.1007/978-3-642-04081-8_19
    Conference Papers | 2009
    McIver A; Meinicke L; Morgan CC, 2009, 'Security, probability and nearly fair coins in the cryptographers' cafe', in Cavalcanti A; Dams D (eds.), Logic Programming, 21st International Conference, Springer, Berlin, pp. 41 - 71, presented at Formal Methods 2009, Eindhoven, Netherlands, 02 November 2009 - 06 November 2009, http://dx.doi.org/10.1007/978-3-642-05089-3_5
    Conference Papers | 2009
    McIver AK; Morgan CC, 2009, 'Sums and Lovers: Case studies in security, compositionality and refinement', in Cavalcanti A; Dams D (eds.), Logic Programming, 21st International Conference, Springer, Berlin, pp. 289 - 304, presented at Formal Methods 2009, Eindhoven, Netherlands, 02 November 2009 - 06 November 2009, http://dx.doi.org/10.1007/978-3-642-05089-3_19
    Conference Papers | 2009
    Morgan CC, 2009, 'How to brew-up a refinement order', in Electronic Notes in Theoretical Computer Science, Elsevier BV, Eindhoven, Netherlands, pp. 123 - 141, presented at REFINE 2009, Eindhoven, Netherlands, 01 November 2009, http://dx.doi.org/10.1016/j.entcs.2009.12.021
    Conference Papers | 2008
    McIver A; Gonzalia C; Morgan CC, 2008, 'Proofs and refutations for probabilistic systems', in Formal methods 2008, Springer, Turku, Finland, pp. 100 - 115, presented at Formal methods 2008, Turku, Finland, 26 May 2008 - 30 May 2008, http://dx.doi.org/10.1007/978-3-540-68237-0_9
    Conference Papers | 2008
    McIver AK; Morgan CC; Conzalia C, 2008, 'Proofs and refutations for probabilistic refinement', in Cuellar J; Maibaum T; Sere K (eds.), FM 2008: FORMAL METHODS, PROCEEDINGS, SPRINGER-VERLAG BERLIN, FINLAND, Turku, pp. 100 - +, presented at 15th International Symposium on Formal Methods, FINLAND, Turku, 26 May 2008 - 30 May 2008, https://www.webofscience.com/api/gateway?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:000256247100009&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=891bb5ab6ba270e68a29b250adbe88d1
    Conference Papers | 2007
    Deng Y; van Glabbeek RJ; Hennessy M; Morgan CC; Zhang C, 2007, 'Characterising testing preorders for finite probabilistic processes', in 22nd Annual IEEE symposium on logic in computer science, Institute of Electrical and Electronics Engineers Inc., 445 Hoes Lane / P.O. Box 1331, Piscataway, NJ 08855-1331, United States, Wroclaw, Poland, pp. 313 - 322, presented at 22nd Annual IEEE symposium on logic in computer science, Wroclaw, Poland, 10 July 2007 - 14 July 2007, http://dx.doi.org/10.1109/LICS.2007.15
    Conference Papers | 2007
    Deng Y; van Glabbeek RJ; Morgan CC; Zhang C, 2007, 'Scalar outcomes suffice for finitary probabilistic testing', in 16th European symposium on programming, 2007, Braga, Portugal, pp. 363 - 378, presented at 16th European symposium on programming, 2007, Braga, Portugal, 24 March 2007 - 01 April 2007
    Conference Papers | 2006
    McIver A; Cohen EG; Morgan CC, 2006, 'Using Probabilistic Kleene algebra for protocol verification', in Maths of Program Construction, Manchester, England, pp. 296 - 310, presented at Maths of Program Construction, Manchester, England, 29 August 2006 - 02 September 2006
    Conference Papers | 2006
    Morgan CC, 2006, 'The shadow knows: refinement of ignorance in sequential programs', in Mathematics of program construction, Kurressare, Estonia, pp. 629 - 653, presented at Mathematics of program construction, Kurressare, Estonia, 03 July 2006 - 05 July 2006, http://dx.doi.org/10.1016/j.scico.2007.09.003
    Conference Papers | 2005
    Hoang TS; Jin Z; Robinson KA; McIver A; Morgan CC, 2005, 'Development via refinement in probabilistic B - Foundation and case study', in 13th International Conference on FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FoSSaCS 2010), Springer-Verlag, Germany, pp. 355 - 373, presented at Formal specification and development in Z and B, Guildford, UK, 13 April 2005 - 15 April 2005, http://dx.doi.org/10.1007/b135596
    Conference Papers | 2005
    Hurd J; McIver A; Morgan CC, 2005, 'Probabilistic Guarded Commands Mechanized in HOL', in Electronic Notes in Theoretical Computer Science, Elsevier BV, Barcelona, Spain, pp. 95 - 111, presented at Quantitative aspects of programming languages 2005, Barcelona, Spain, 29 November 2005 - 01 December 2005, http://dx.doi.org/10.1016/j.entcs.2004.01.021
    Conference Papers | 2005
    Morgan CC; McIver A, 2005, 'A novel stochastic game via the quantitative modal mu-calculus', in Electronic Notes in Theoretical Computer Science, Elsevier BV, Edinburgh, Scotland, pp. 195 - 212, presented at Quantitative Aspects of Programming Languages 2006, Edinburgh, Scotland, 02 April 2005 - 03 April 2005, http://dx.doi.org/10.1016/j.entcs.2005.10.039
    Conference Papers | 2005
    Morgan CC; McIver AK, 2005, 'Programming-logic analysis of fault tolerance: Expected performance of self-stabilisation', in Butler M; Jones C; Romanovsky A; Troubitsyna E (eds.), RIGOROUS DEVELOPMENT OF COMPLEX FAULT-TOLERANT SYSTEMS, SPRINGER-VERLAG BERLIN, ENGLAND, Newcastle Univ, Newcastle upon Tyne, pp. 288 - +, presented at Workshop on Rigorous Open Development Environment for Complex Systems, ENGLAND, Newcastle Univ, Newcastle upon Tyne, https://www.webofscience.com/api/gateway?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:000244663400015&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=891bb5ab6ba270e68a29b250adbe88d1
    Conference Papers | 2004
    Morgan CC; McIver A; He J, 2004, 'Deriving Probabilistic Semantics vis the Weakest Completion', in 6th International Conference on Formal Engineering Methods, ICFEM 2004, Springer, Seattle, Washington, USA, pp. 131 - 145, presented at 6th International Conference on Formal Engineering Methods, ICFEM 2004, Seattle, Washington, USA, 08 November 2004 - 12 November 2004
    Conference Papers | 2004
    Morgan CC; McIver A, 2004, 'Memoryless strategies for stochastic games via domain theory', in Electronic Notes in Theoretical Computer Science, Elsevier BV, Recife, pp. 23 - 37, presented at Brazilian Symposium on Formal Methods 2004, Recife, http://dx.doi.org/10.1016/j.entcs.2005.03.003
    Conference Papers | 2003
    Morgan CC; McIver A; Hoang TS; Robinson KA; Jin Z, 2003, 'Probabilistic invariants for probabilistic machines', in ZB 2003: Formal Specification and develoment in B and Z, Springer, Turku, Finland, pp. 240 - 259, presented at ZB 2003: Formal Specification and develoment in B and Z, Turku, Finland, http://dx.doi.org/10.1007/3-540-44880-2_16
    Conference Papers | 2003
    Morgan CC; McIver A; Hoang TS, 2003, 'Probabilistic Termination in B', in ZB 2003: Formal Specification and develoment in B and Z, Springer, Turku, Finland, pp. 216 - 239, presented at ZB 2003: Formal Specification and develoment in B and Z, Turku, Finland, http://dx.doi.org/10.1007/3-540-44880-2_15
    Conference Papers | 2002
    Morgan CC, 2002, 'Games, probability and the quantitative mu-calculus qMu', in Logic for Programming, Artificial Intelligence and Reasoning LNAI 2514, Springer, Tbilisi Georgia, pp. 292 - 310, presented at Logic for Programming, Artificial Intelligence and Reasoning, Tbilisi Georgia, 14 October 2002 - 18 October 2002, http://dx.doi.org/10.1007/3-540-36078-6_20
    Conference Papers | 1998
    Morgan C, 1998, 'The generalised substitution language extended to probabilistie programs', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 9 - 25, http://dx.doi.org/10.1007/bfb0053351
    Conference Papers | 1990
    Woodcock JCP; Morgan C, 1990, 'Refinement of state-based concurrent systems', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 340 - 351, http://dx.doi.org/10.1007/3-540-52513-0_18
    Conference Papers | 1989
    Morgan C, 1989, 'Types and invariants in the refinement calculus', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 363 - 378, http://dx.doi.org/10.1007/3-540-51305-1_22
    Conference Papers | 1985
    Morgan C; Hoare CAR, 1985, 'Specification of a simplified network service in CSP (Problem 2)', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 345 - 353, http://dx.doi.org/10.1007/3-540-16047-7_56
    Conference Papers | 1985
    Morgan C, 1985, 'Specification of a simplified network service in Z (Problem 2)', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 318 - 344, http://dx.doi.org/10.1007/3-540-16047-7_55

Quantitative information flow (cyber-security); differential privacy; concurrency and Formal Methods generally.