By Emeritus Professor Carroll Morgan

Journal articles

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

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

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

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

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

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

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

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

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

McIver A; Morgan CC, 2010, 'Compositional refinement in agent-based security protocols', Formal Aspects of Computing, http://dx.doi.org/10.1007/s00165-010-0164-1

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

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

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

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

McIver A; Morgan CC, 2007, 'Results on the quantitative mu-calculus qM mu', ACM Transactions on Computational Logic, 8, pp. 3:1 - 3:43

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

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

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

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

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

Morgan CC; McIver A, 2003, 'Almost-certain eventualities and abstract probabilities in quantitative temporal logic', Theoretical Computer Science, 293, pp. 507 - 534

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

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

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

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

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, pp. 30 - 36

Seidel K; Morgan C, 1997, 'Hierarchical Reasoning in Probabilistic CSP', Programming and Computer Software, 23, pp. 239 - 250

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

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

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

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

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

Morgan C, 1994, 'Foreword', Science of Computer Programming, 22, pp. 1 - 2, http://dx.doi.org/10.1016/0167-6423(94)90004-3

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

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

Morgan C; Gardiner PHB, 1990, 'Data refinement by calculation', Acta Informatica, 27, pp. 481 - 503, http://dx.doi.org/10.1007/BF00277386

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

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

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

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

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

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

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

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

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

Conference Papers

Chen C; McIver A; Morgan C, 2025, 'Probabilistic Datatypes', in Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, pp. 3 - 16, http://dx.doi.org/10.1007/978-3-031-77019-7_1

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

Alvim MS; Fernandes N; McIver A; Morgan C; Nunes GH, 2021, 'A Novel Analysis of Utility in Privacy Pipelines, Using Kronecker Products and Quantitative Information Flow', in Ccs 2023 Proceedings of the 2023 ACM Sigsac Conference on Computer and Communications Security, pp. 1718 - 1731, http://dx.doi.org/10.1145/3576915.3623081

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

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

Back to profile page