By Emeritus Professor Carroll Morgan

Journal articles

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

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

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', 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

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

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

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

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

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

Back to profile page