A prime decomposition result for parallel systems. - Carroll Morgan (SIGACT News, 1976)

Specification of a simplified Network Service in Z. - Carroll Morgan (The Analysis of Concurrent Systems, 1983)

Specification of a simplified Network Service in CSP. - Carroll Morgan; C. A. R. Hoare (The Analysis of Concurrent Systems, 1983)

Specification of the UNIX Filing System. - Carroll Morgan; Bernard Sufrin (IEEE Trans. Software Eng., 1984)

Global and Logical Time in Distributed Algorithms. - Carroll Morgan (Inf. Process. Lett., 1985)

Laws of Programming. - C. A. R. Hoare; Ian J. Hayes; Jifeng He 001; Carroll Morgan; A. W. Roscoe 001; Jeff W. Sanders; Ib Holm Sørensen; J. Michael Spivey; Bernard Sufrin (Commun. ACM, 1987)

Data Refinement by Miracles. - Carroll Morgan (Inf. Process. Lett., 1988)

Auxiliary Variables in Data Refinement. - Carroll Morgan (Inf. Process. Lett., 1988)

Procedures, parameters, and abstraction: Separate concerns. - Carroll Morgan (Sci. Comput. Program., 1988)

The Specification Statement. - Carroll Morgan (ACM Trans. Program. Lang. Syst., 1988)

Types and Invariants in the Refinement Calculus. - Carroll Morgan (MPC, 1989)

Programming from specifications. - Carroll Morgan (Prentice Hall, 1990)

Refinement of State-Based Concurrent Systems. - Jim Woodcock 001; Carroll Morgan (VDM Europe, 1990)

Data Refinement by Calculation. - Carroll Morgan; Paul H. B. Gardiner (Acta Informatica, 1990)

Types and Invariants in the Refinement Calculus. - Carroll Morgan; Trevor Vickers (Sci. Comput. Program., 1990)

Data Refinement of Predicate Transformers. - Paul H. B. Gardiner; Carroll Morgan (Theor. Comput. Sci., 1991)

The Refinement Calculus. - Carroll Morgan (NATO ASI PDC, 1992)

The Refinement Calculus, and Literate Development. - Carroll Morgan (Formal Program Development, 1993)

A Single Complete Rule for Data Refinement. - Paul H. B. Gardiner; Carroll Morgan (Formal Aspects Comput., 1993)

Programming from specifications, 2nd Edition. - Carroll Morgan (Prentice Hall, 1994)

Foreword: Special Issue on Mathematics of Program Construction. - Carroll Morgan (Sci. Comput. Program., 1994)

Action Systemes, Unbounded Nondeterminism, and Infinite Traces. - Michael J. Butler; Carroll Morgan (Formal Aspects Comput., 1995)

Exits in the Refinement Calculus. - Steve King 001; Carroll Morgan (Formal Aspects Comput., 1995)

Refinement-Oriented Probability for CSP. - Carroll Morgan; Annabelle McIver; Karen Seidel 002; Jeff W. Sanders (Formal Aspects Comput., 1996)

Unifying wp and wlp. - Carroll Morgan; Annabelle McIver (Inf. Process. Lett., 1996)

Probabilistic Predicate Transformers. - Carroll Morgan; Annabelle McIver; Karen Seidel 002 (ACM Trans. Program. Lang. Syst., 1996)

The Generalised Substitution Language Extended to Probabilistic Programs. - Carroll Morgan (B, 1998)

An Expectation-Transformer Model for Probabilistic Temporal Logic. - Carroll Morgan; Annabelle McIver (Log. J. IGPL, 1999)

An Iterator Construct for the Refinement Calculus. - Steve King 001; Carroll Morgan (IWFM, 2000)

Cost Analysis of Games, Using Program Logic. - Carroll Morgan; Annabelle McIver (APSEC, 2001)

Demonic, angelic and unbounded probabilistic choices in sequential programs. - Annabelle McIver; Carroll Morgan (Acta Informatica, 2001)

Almost-Certain Eventualities and Abstract Probabilities in the Temporal Logic PTL. - Annabelle McIver; Carroll Morgan (CATS, 2001)

Partial correctness for probabilistic demonic programs. - Annabelle McIver; Carroll Morgan (Theor. Comput. Sci., 2001)

Games, Probability and the Quantitative µ-Calculus qMµ. - Annabelle McIver; Carroll Morgan (LPAR, 2002)

Probabilistic Invariants for Probabilistic Machines. - Thai Son Hoang; Zhendong Jin; Ken Robinson; Annabelle McIver; Carroll Morgan (ZB, 2003)

Probabilistic Termination in B. - Annabelle McIver; Carroll Morgan; Thai Son Hoang (ZB, 2003)

Results on the quantitative mu-calculus qMu - Annabelle McIver; Carroll Morgan (CoRR, 2003)

Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL. - Annabelle McIver; Carroll Morgan (Theor. Comput. Sci., 2003)

Of Probabilistic Wp and SP-and Compositionality. - Carroll Morgan (25 Years Communicating Sequential Processes, 2004)

Deriving Probabilistic Semantics Via the 'Weakest Completion'. - Jifeng He 001; Carroll Morgan; Annabelle McIver (ICFEM, 2004)

Developing and Reasoning About Probabilistic Programs in pGCL. - Annabelle McIver; Carroll Morgan (PSSE, 2004)

Memoryless Strategies for Stochastic Games via Domain Theory. - Carroll Morgan; Annabelle McIver (SBMF, 2004)

Development via Refinement in Probabilistic B - Foundation and Case Study. - Thai Son Hoang; Zhendong Jin; Ken Robinson; Annabelle McIver; Carroll Morgan (ZB, 2005)

The Challenge of Probabilistic Event B - Extended Abstract. - Carroll Morgan; Thai Son Hoang; Jean-Raymond Abrial (ZB, 2005)

A Novel Stochastic Game Via the Quantitative mu-calculus. - Annabelle McIver; Carroll Morgan (QAPL, 2005)

An elementary proof that Herman's Ring is Theta (N2). - Annabelle McIver; Carroll Morgan (Inf. Process. Lett., 2005)

Abstraction and refinement in probabilistic systems. - Annabelle McIver; Carroll Morgan (SIGMETRICS Perform. Evaluation Rev., 2005)

Probabilistic guarded commands mechanized in HOL. - Joe Hurd; Annabelle McIver; Carroll Morgan (Theor. Comput. Sci., 2005)

Abstraction, Refinement and Proof for Probabilistic Systems - Annabelle McIver; Carroll Morgan (Springer, 2005)

Using Probabilistic Kleene Algebra for Protocol Verification. - Annabelle McIver; Ernie Cohen; Carroll Morgan (RelMiCS, 2006)

The Shadow Knows: Refinement of Ignorance in Sequential Programs. - Carroll Morgan (MPC, 2006)

Programming-Logic Analysis of Fault Tolerance: Expected Performance of Self-stabilisation. - Carroll Morgan; Annabelle McIver (RODIN Book, 2006)

Scalar Outcomes Suffice for Finitary Probabilistic Testing. - Yuxin Deng; Rob J. van Glabbeek; Carroll Morgan; Chenyi Zhang 001 (ESOP, 2007)

Characterising Testing Preorders for Finite Probabilistic Processes. - Yuxin Deng; Rob J. van Glabbeek; Matthew Hennessy; Carroll Morgan; Chenyi Zhang 001 (LICS, 2007)

Remarks on Testing Probabilistic Processes. - Yuxin Deng; Rob J. van Glabbeek; Matthew Hennessy; Carroll Morgan; Chenyi Zhang 001 (Computation, Meaning, and Logic, 2007)

Results on the quantitative µ-calculus qMµ. - Annabelle McIver; Carroll Morgan (ACM Trans. Comput. Log., 2007)

Proofs and Refutations for Probabilistic Refinement. - A. K. McIver; Carroll C. Morgan; Carlos Gonzalía (FM, 2008)

Using probabilistic Kleene algebra pKA for protocol verification. - A. K. McIver; Carlos Gonzalía; Ernie Cohen; Carroll C. Morgan (J. Log. Algebraic Methods Program., 2008)

Characterising Testing Preorders for Finite Probabilistic Processes. - Yuxin Deng; Rob J. van Glabbeek; Matthew Hennessy; Carroll Morgan (Log. Methods Comput. Sci., 2008)

Testing Finitary Probabilistic Processes. - Yuxin Deng; Rob J. van Glabbeek; Matthew Hennessy; Carroll Morgan (CONCUR, 2009)

Sums and Lovers: Case Studies in Security, Compositionality and Refinement. - Annabelle McIver; Carroll C. Morgan (FM, 2009)

Security, Probability and Nearly Fair Coins in the Cryptographers' Café. - Annabelle McIver; Larissa Meinicke; Carroll Morgan (FM, 2009)

How to Brew-up a Refinement Ordering. - Carroll Morgan (REFINE@FMWeek, 2009)

The Shadow Knows: Refinement and security in sequential programs. - Carroll Morgan (Sci. Comput. Program., 2009)

The Thousand-and-One Cryptographers. - A. K. McIver; Carroll C. Morgan (Reflections on the Work of C. A. R. Hoare, 2010)

Compositional Closure for Bayes Risk in Probabilistic Noninterference. - Annabelle McIver; Larissa Meinicke; Carroll Morgan (ICALP (2), 2010)

Linear-Invariant Generation for Probabilistic Programs: - Automated Support for Proof-Based Methods. - Joost-Pieter Katoen; Annabelle McIver; Larissa Meinicke; Carroll C. Morgan (SAS, 2010)

Real-Reward Testing for Probabilistic Processes (Extended Abstract) - Yuxin Deng; Rob J. van Glabbeek; Matthew Hennessy; Carroll Morgan (QAPL, 2011)

Compositional refinement in agent-based security protocols. - A. K. McIver; Carroll C. Morgan (Formal Aspects Comput., 2011)

A Kantorovich-Monadic Powerdomain for Information Hiding, with Probability and Nondeterminism. - Annabelle McIver; Larissa Meinicke; Carroll Morgan (LICS, 2012)

Elementary Probability Theory in the Eindhoven Style. - Carroll Morgan (MPC, 2012)

Compositional noninterference from first principles. - Carroll Morgan (Formal Aspects Comput., 2012)

Quantitative methods in security and safety critical applications (NII Shonan Meeting 2012-10). - Jin Song Dong; Annabelle McIver; Carroll Morgan (NII Shonan Meet. Rep., 2012)

Lattices of Information for Security: Deterministic, Demonic, Probabilistic. - Carroll C. Morgan (ICFEM, 2013)

Additive and Multiplicative Notions of Leakage, and Their Capacities. - Mário S. Alvim; Konstantinos Chatzikokolakis 001; Annabelle McIver; Carroll Morgan; Catuscia Palamidessi; Geoffrey Smith 001 (CSF, 2014)

Towards a Formal Analysis of Information Leakage for Signature Attacks in Preferential Elections. - Roland Wen; Annabelle McIver; Carroll Morgan (FM, 2014)

Abstract Channels and Their Robust Information-Leakage Ordering. - Annabelle McIver; Carroll Morgan; Geoffrey Smith 001; Barbara Espinoza; Larissa Meinicke (POST, 2014)

(In-)Formal Methods: The Lost Art - A Users' Manual. - Carroll Morgan (SETSS, 2014)

Abstractions of non-interference security: probabilistic versus possibilistic. - Thai Son Hoang; A. K. McIver; Larissa Meinicke; Carroll C. Morgan; Anthony Sloane; E. Susatyo (Formal Aspects Comput., 2014)

An old new notation for elementary probability theory. - Carroll Morgan (Sci. Comput. Program., 2014)

Selected papers from the Brazilian Symposium on Formal Methods (SBMF 2011). - Adenilso da Silva Simão; Carroll Morgan (Sci. Comput. Program., 2014)

Real-reward testing for probabilistic processes. - Yuxin Deng; Rob J. van Glabbeek; Matthew Hennessy; Carroll Morgan (Theor. Comput. Sci., 2014)

Controlled Owicki-Gries Concurrency: Reasoning about the Preemptible eChronos Embedded Operating System. - June Andronick; Corey Lewis; Carroll Morgan (MARS, 2015)

Hidden-Markov program algebra with iteration. - Annabelle McIver; Larissa Meinicke; Carroll Morgan (Math. Struct. Comput. Sci., 2015)

Axioms for Information Leakage. - Mário S. Alvim; Konstantinos Chatzikokolakis 001; Annabelle McIver; Carroll Morgan; Catuscia Palamidessi; Geoffrey Smith 001 (CSF, 2016)

Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency. - June Andronick; Corey Lewis; Daniel Matichuk; Carroll Morgan; Christine Rizkallah (ITP, 2016)

Compositional security and collateral leakage. - Nicolás E. Bordenabe; Annabelle McIver; Carroll Morgan; Tahiry M. Rabehaja (CoRR, 2016)

A new rule for almost-certain termination of probabilistic and demonic programs. - Annabelle McIver; Carroll Morgan (CoRR, 2016)

Algebra for Quantitative Information Flow. - Annabelle McIver; Carroll C. Morgan; Tahiry M. Rabehaja (RAMiCS, 2017)

A Demonic Lattice of Information. - Carroll Morgan (Concurrency, Security, and Puzzles, 2017)

Reasoning About Distributed Secrets. - Nicolás E. Bordenabe; Annabelle McIver; Carroll Morgan; Tahiry M. Rabehaja (FORTE, 2017)

Privacy in elections: How small is "small"? - Annabelle McIver; Tahiry M. Rabehaja; Roland Wen; Carroll Morgan (J. Inf. Secur. Appl., 2017)

A new proof rule for almost-sure termination. - Annabelle McIver; Carroll Morgan; Benjamin Lucien Kaminski; Joost-Pieter Katoen (Proc. ACM Program. Lang., 2018)

Proving that Programs Are Differentially Private. - Annabelle McIver; Carroll Morgan (APLAS, 2019)

Categorical Information Flow. - Tahiry M. Rabehaja; Annabelle McIver; Carroll Morgan; Georg Struth (The Art of Modelling Computational Systems, 2019)

Program algebra for quantitative information flow. - A. K. McIver; Carroll C. Morgan; T. M. Rabehaja (J. Log. Algebraic Methods Program., 2019)

Abstract Hidden Markov Models: a monadic account of quantitative information flow. - Annabelle McIver; Carroll Morgan; Tahiry M. Rabehaja (Log. Methods Comput. Sci., 2019)

An axiomatization of information flow measures. - Mário S. Alvim; Konstantinos Chatzikokolakis 001; Annabelle McIver; Carroll Morgan; Catuscia Palamidessi; Geoffrey Smith 001 (Theor. Comput. Sci., 2019)

Quantitative Information Flow with Monads in Haskell. - Jeremy Gibbons; Annabelle McIver; Carroll Morgan; Tom Schrijvers (Foundations of Probabilistic Programming, 2020)

Correctness by Construction for Probabilistic Programs. - Annabelle McIver; Carroll Morgan (ISoLA (1), 2020)

Preface. - Peter Höfner; Carroll Morgan; Vaughan R. Pratt (Acta Informatica, 2020)

The Science of Quantitative Information Flow. - Mário S. Alvim; Konstantinos Chatzikokolakis 001; Annabelle McIver; Carroll Morgan; Catuscia Palamidessi; Geoffrey Smith 001 (Springer, 2020)

The Laplace Mechanism has optimal utility for differential privacy over continuous queries. - Natasha Fernandes; Annabelle McIver; Carroll Morgan (LICS, 2021)

Algorithmics. - Richard S. Bird; Jeremy Gibbons; Ralf Hinze; Peter Höfner; Johan Jeuring; Lambert G. L. T. Meertens; Bernhard Möller; Carroll Morgan; Tom Schrijvers; Wouter Swierstra; Nicolas Wu (IFIP's Exciting First 60+ Years, 2021)

How to Develop an Intuition for Risk... and Other Invisible Phenomena (Invited Talk). - Natasha Fernandes; Annabelle McIver; Carroll Morgan (CSL, 2022)

Flexible and scalable privacy assessment for very large datasets, with an application to official governmental microdata. - Mário S. Alvim; Natasha Fernandes; Annabelle McIver; Carroll Morgan; Gabriel Henrique Nunes (Proc. Priv. Enhancing Technol., 2022)

A Novel Analysis of Utility in Privacy Pipelines, Using Kronecker Products and Quantitative Information Flow. - Mário S. Alvim; Natasha Fernandes; Annabelle McIver; Carroll Morgan; Gabriel Henrique Nunes (CCS, 2023)

Source-Level Reasoning for Quantifying Information Leaks. - Chris Chen; Annabelle McIver; Carroll Morgan (Principles of Verification (1), 2024)

Probabilistic Datatypes. - Chris Chen; Annabelle McIver; Carroll Morgan (ICTAC, 2024)

Source-level reasoning for quantitative information flow. - Chris Chen; Annabelle McIver; Carroll Morgan (CoRR, 2024)

On Formal Methods Thinking in Computer Science Education. - Brijesh Dongol; Catherine Dubois; Stefan Hallerstede; Eric C. R. Hehner; Carroll Morgan; Peter Müller 001; Leila Ribeiro 001; Alexandra Silva 001; Graeme Smith 001; Erik P. de Vink (Formal Aspects Comput., 2025)

Forward and Backward Simulations for Partially Observable Probability. - Chris Chen; Annabelle McIver; Carroll Morgan (CoRR, 2025)