A selection of recent publications:     McIver:15, Morgan:13, McIver:12, McIver:11a, Katoen:10 and McIver:10.

Texts, book chapters and summer-school presentations

Abstraction, refinement and proof for probabilistic systems. A tutorial and reference guide to the principal publications. Springer Verlag Monographs in Computer Science Published January 2005 (sample pages)

Invited book chapters:

• The Thousand-and-One Cryptographers. 2010.
• Remarks on Testing Probabilistic Processes. 2007.
• Programming-Logic Analysis of Fault Tolerance. 2006.
• Developing and Reasoning about Probabilistic Programs in pGCL. 2006.
• Abstraction and Refinement of Probabilistic Systems. 2005.
• Of Probabilistic wp and CSP. 2005.
• A Probabilistic Approach to Information Hiding. 2003.
• Probably Hoare? Hoare Probably!. 2000.

Presentations:

• Expectation-based reasoning for sequential probabilistic programs
• Lectures on probabilistic formal methods
• Lectures on probabilistic formal methods
• Formal methods for probabilistic systems
• Seminar series on probabilistic semantics
• Graduate course on probabilistic semantics (MIT)

Themes

The publications are grouped by themes. Within each theme the order is most-to-least recent:

• Tutorials, examples and case studies;
• Probabilistic process algebra;
• Probability and nondeterminism in sequential programming;
• Stochastic games; quantitative modal- and temporal logic;
• Information security and anonymity;
• Quantum computation;
• Theorem proving and model checking;
• Probabilistic algebra;
• Applications;
• Informal notes, and work in progress;
• Related work.

Tutorials, examples and case studies

Within topic the articles are most-to least recent; hovering will reveal their titles.

Probabilistic process algebra

Deng:07b

Characterising Testing Preorders for Finite Probabilistic Processes
Y. Deng, R. van Glabbeek, M. Hennessy, C. Morgan, and C. Zhang
in Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, 313-325
LICS '07 , IEEE Computer Society (2007)

Deng:07a

Remarks on Testing Probabilistic Processes
Y. Deng, R. van Glabbeek, M. Hennessy, C. C. Morgan, and C. Zhang
in Computation, Meaning, and Logic: Articles Dedicated to Gordon Plotkin, L. Cardelli et al. (Ed.), 359–97
ENTCS 172, Elsevier  (2007)

Deng:07

Scalar Outcomes Suffice for Finitary Probabilistic Testing
Y. Deng, R. van Glabbeek, C. C. Morgan, and C. Zhang
in Proc ESOP ’07, De Nicola (Ed.),
LNCS , Springer (2007)

Morgan:05

Of Probabilistic wp and CSP
C. C. Morgan
Communicating Sequential Processes: The First 25 Years, A. Abdallah and C.B. Jones and J.W. Sanders (Ed.), , Springer  (2005)

Seidel:97

Hierarchical Reasoning in Probabilistic CSP
K. Seidel and C. C. Morgan
Programmirovanie (Russian journal of Programming and Computer Software) 23(5)
Mezhdunarodnaya Kniga (1997)

Morgan:96c

Refinement-Oriented Probability for CSP
C. C. Morgan, A. K. McIver, K. Seidel, and J. W. Sanders
Formal Aspects of Computing 8(6):617–47
Springer (1996)

Seidel:95

Probabilistic Communicating Processes
K. Seidel
Theo Comp Sci 152(2)
Elsevier (1995)

Morgan:95

Argument Duplication in Probabilistic CSP
C. C. Morgan, A. K. McIver, K. Seidel, and J. W. Sanders
PRG Technical Report  PRG-TR-11-95  Oxford University (1995)

McIver:95

Probabilistic Determinism in PCSP
A. K. McIver, C. C. Morgan, K. Seidel, and J. W. Sanders
PRG Technical Report  PRG-TR-13-95  Oxford University (1995)

Seidel:92

Probabilistic Communicating Processes
K. Seidel
PRG Technical Monograph  PRG-102  Oxford University (1992)
See also Seidel:95.

See also Deng:07b.

Information security and anonymity

McIver:15

Abstract Hidden Markov Models: a monadic account of quantitative information flow
A. McIver, C. Morgan and T. Rabehaja
Proc. LiCS 2015
To appear. 

Morgan:13

An Old New Notation for Elementary Probability Theory
C. Morgan
  Under review      (2013)

Morgan:12

Elementary probability theory in the Eindhoven style
C. Morgan
Proc. MPC 2012, (2012)
Explains and motivates the specialised notation used in McIver:11 and McIver:10.

McIver:12

A Kantorovich-Monadic Powerdomain for Information Hiding, with Probability and Nondeterminism
A. McIver, L. Meinicke, and C. Morgan
Proc. LiCS 2012, Nachum Derschowitz (Ed.), IEEE (2012)

McIver:11

Hidden-{Markov} Program Algebra with Iteration
A. McIver and L. Meinicke and C. Morgan
To appear in Mathematical Structures in Computer Science in 2012

Morgan:10

Compositional noninterference from first principles
C. Morgan
Formal Aspects of Computing 24(1):1-24
Springer (2010)

McIver:10b

Compositional refinement in agent-based security protocols
A. McIver and C. Morgan
Formal Aspects of Computing 23(6):1-27
Springer (2010)

McIver:10

Compositional closure for Bayes Risk in probabilistic noninterference
A. McIver, L. Meinicke, and C. Morgan
in Proceedings of the 37th international colloquium conference on Automata, languages and programming: Part II, (Ed.), 223--235
ICALP'10 6199, Springer (2010)
Full version available at McIver:10a.

McIver:09f

Security, Probability and Nearly Fair Coins in the Cryptographers' Café
A. K. McIver, L. A. Meinicke, and C. C. Morgan
in Proc FM '09, A. Cavalcanti and D. Dams (Ed.),
LNCS 5850, Springer (2009)

McIver:09b

Sums and Lovers: Case Studies in Security, Compositionality and Refinement
A. K. McIver and C. C. Morgan
in Proc. FM '09, A. Cavalcanti and D. Dams (Ed.),
LNCS 5850, Springer (2009)
Case Study: Multi-party computation: The Millionaires’ Problem

Morgan:09

How to Brew-Up a Refinement Ordering
C. C. Morgan
in Proc International Refinement Workshop, Eindhoven, E. Boiten and J. Derrick and S. Reeves (Ed.), 123--41
ENTCS 259, (2009)
See also Morgan:10.

McIver:10c

The Thousand-and-One Cryptographers
A. K. McIver and C. C. Morgan
Reflections on the Work of C.A.R. Hoare, Cliff B. Jones and A.W. Roscoe and Kenneth R. Wood (Ed.), , Springer  (2010)
Case Study: Unboundedly many Dining Cryptographers

Morgan:09a

The Tale of the Three Judges
C. Morgan
  Presentation accompanying Festschrift in Honour of Tony Hoare  (2009)
Case Study: The Three-Judges anonymity protocol

McIver:09d

The Secret Art of Computer Programming
A. K. McIver
in Proc. ICTAC 2009, (Ed.), 61--78
LNCS 5684, (2009)

McIver:08a

A Calculus of Revelations
A. K. McIver and C. C. Morgan
    Presentation at VSTTE 2008, Toronto  (2008)
Case Study: Unboundedly many Dining Cryptographers

Morgan:07

The Shadow Knows: Refinement of Ignorance in Sequential Programs
C. C. Morgan
Science of Computer Programming 74(8):629--653
Elsevier (2009)
See also Morgan:06.

Morgan:06

The Shadow Knows: Refinement of Ignorance in Sequential Programs
C. C. Morgan
in Math Prog Construction, T. Uustalu (Ed.), 359–78
Springer 4014, Springer (2006)
See also Morgan:07.

McIver:03b

A Probabilistic Approach to Information Hiding
A. K. McIver and C. C. Morgan
in Programming Methodology: A Collection of Essays by the IFIP WG2.3 Membership, A.K. McIver and C.C. Morgan (Ed.),
Tech Mono Comp Sci , Springer  (2003)

Robinson:98

Restricted Demonic Choice for Modular Probabilistic Programs
D. Robinson and C. C. Morgan
ESSLI PLRC Workshop '98  (1998)

See also McIver:10, Morgan:10, Morgan:98a & McIver:98a.

Quantum computation

Zuliani:09

Reasoning about Faulty Quantum Programs
P. Zuliani
Acta Inf 46(6):403--32
Springer (2009)

Zuliani:05

Compiling Quantum Programs
P. Zuliani
Acta Inf 41(7):435–74
Springer (2005)

Zuliani:01a

Logical Reversability
P. Zuliani
IBM Jnl Res Dev 45(6)
IBM (2001)

Zuliani:01

Quantum Programming
P. Zuliani
DPhil Thesis Oxford University (2001)

Zuliani:01b

Formal Reasoning for Quantum-Mechanical Non-Locality
P. Zuliani
Research Report  RR-01-05  Oxford University (2001)

Sanders:00

Quantum Programming
J. W. Sanders and P. Zuliani
in Proc MPC ’00, R. Backhouse and J. Oliviera (Ed.), 80–99
LNCS 1837, Springer (2000)

Theorem proving and model checking

Ndukwu:11

Model exploration and analysis for quantitative safety refinement in probabilistic B
U. Ndukwu and A. McIver
in Refine, John Derrick and Eerke A. Boiten and Steve Reeves (Ed.), 101-120
EPTCS 55, (2011)

Ndukwu:10a

YAGA: Automated Analysis of Quantitative Safety Specifications in Probabilistic B
U. Ndukwu and A. K. McIver
in ATVA, Ahmed Bouajjani and Wei-Ngan Chin (Ed.), 378-386
Lecture Notes in Computer Science 6252, Springer (2010)

Ndukwu:10

An expectation transformer approach to predicate abstraction and data independence for probabilistic programs
U. Ndukwu and A. McIver
in QAPL, Alessandra Di Pierro and Gethin Norman (Ed.), 129-143
EPTCS 28, (2010)

Katoen:10

Linear-Invariant Generation for Probabilistic Programs: Automated Support for Proof-Based Methods
J.-P. Katoen, A. K. McIver, L. A. Meinicke, and C. C. Morgan
Proc. Static Analysis Symp., (Ed.), 390--406, Springer (2010)

McIver:09e

Probabilistic Affirmation and Refutation: Case Studies
A. McIver, C. Gonzalia, and C. Gonzalia
Proc. Automatic Program Verification, (Ed.), , (2009)

McIver:2008yq

Proofs and Refutations for Probabilistic Systems
A. K. McIver, C. C. Morgan, and C. Gonzalia
in Proc FM '08, T. Maibaum and J. Cuellar (Ed.),
LNCS 5014, Springer (2008)
Awarded Best Paper

Fruth:07

Graphical Modelling for Simulation and Formal Analysis of Wireless Networked Protocols
M. Fruth, A. Fehnker, and A. K. McIver
Proc Workshop Methods, Models and Tools for Fault Tolerance, (Ed.), , (2007)

Gonzalia:07a

Automating Refinement Checking in Probabilistic System Design
C. Gonzalia and A. McIver
in ICFEM, Michael Butler and Michael G. Hinchey and Maria M. Larrondo-Petrie (Ed.), 212-231
Lecture Notes in Computer Science 4789, Springer (2007)

Celiku:06

Mechanized Reasoning for Dually-Nondeterministic and Probabilistic Programs
O. Celiku
PhD thesis  TUCS, Abo Akademi (2006)

McIver:06b

Quantitative Refinement and Model Checking for the Analysis of Probabilistic Systems
A. K. McIver
in Proc FM ’06, J Misra and T. Nipkow and E. Sekerinski (Ed.),
LNCS 4085, Springer (2006)

Hoang:05a

The Development of a Probabilistic B-Method and a Supporting Toolkit
T. S. Hoang
PhD Thesis University of New South Wales (2005)

McIver:05e

Towards Automated Proof Support for Probabilistic Distributed Systems
A. K. McIver and T. Weber
in Proc LPAR 2005, A. Voronkov (Ed.),
LNAI 3835, Springer (2005)

Hoang:05

Refinement in Probabilistic B: Foundation and Case Study
T. S. Hoang, C. C. Morgan, K. A. Robinson, and Z. D. Jin
in Proc ZB 2005, H. Treharne and S. Schneider (Ed.),
LNCS 3455, Springer (2005)

Hurd:05a

Probabilistic Guarded Commands Mechanised in HOL
J. Hurd, A. K. McIver, and C. C. Morgan
Theo Comp Sci 346(1):96–112  (2005)

Hurd:05

Probabilistic Guarded Commands Mechanised in HOL
J. Hurd, A. K. McIver, and C. C. Morgan
in Proc 4th QAPL, A. Cerone and A. de Pierro (Ed.),
ENTCS 112, Elsevier (2005)

Celiku:04

Cost-Based Analysis of Probabilistic Programs Mechanised in HOL
O. Celiku and A. McIver
Nordic Jnl Comp 11(2):102–128
Pub Assoc Nord Jnl Comp (2004)

McIver:03

Probabilistic Termination in B
A. K. McIver, C. C. Morgan, and T. S. Hoang
in Proc ZB ’03, D. Bert and J.P.Bowen and S. King and M. Walden (Ed.), 216–239
LNCS 2651, Springer (2003)
Awarded Best Paper

Hoang:03

Probabilistic Invariants for Probabilistic Machines
T. S. Hoang, A. K. McIver, C. C. Morgan, K. A. Robinson, and Z. D. Jin
in , D. Bert (Ed.),
LNCS 2651, Springer (2003)

Hurd:a

A Formal Approach to Probabilistic Termination
J. Hurd
in TPHOL 2002, Victor A. Carreno and Cesar A. Munoz and Sofiene Tahar (Ed.), 230–45
LNCS 2410, Springer (2002)

See also Hallerstede:07.

Probabilistic algebra

McIver:11a

On Probabilistic Kleene Algebras, Automata and Simulations
A. McIver, T. M. Rabehaja, and G. Struth
in RAMICS, Harrie C. M. de Swart (Ed.), 264-279
Lecture Notes in Computer Science 6663, Springer (2011)

McIver:08

Using Probabilistic Kleene Algebra pKA for Protocol Verification
A. K. McIver, E. Cohen, C. Morgan, and C. Gonzalia
Journal of Logic and Algebraic Programming 76(1):90--111
 (2008)

Cohen:06

Probabilistic Kleene Algebra: Introduction and Example
E. Cohen, A. K. McIver, and C. C. Morgan
in Relations and Kleene Algebra in Computer Science, Renate Schmidt (Ed.),
LNCS 4136, Springer (2006)

McIver:01

A Generalisation of Stationary Distributions, and Probabilistic Program Algebra
A. K. McIver
in Proc 17th Conf Foundations Prog Semantics, Stephen Brookes and Michael Mislove (Ed.),
ENTCS 45, Elsevier  (2001)

See also McIver:07a.

Applications

McIver:06d

Formal Techniques for the Analysis of Wireless Networks
A. McIver and A. Fehnker
Proc 2nd Int Symp ISOLA, T. Margaria and A. Philippou and B. Steffen (Ed.) (2006)

McIver:06c

Quantitative Mu-calculus Analysis of Power Management in Wireless Networks
A. K. McIver
in Proc ICTAC 06, Ana Cavalcanti (Ed.),
LNCS 4281, Springer (2006)

McIver:06

Programming-Logic Analysis of Fault Tolerance
A. K. McIver and C. C. Morgan
Rigorous Development of Complex Fault-Tolerant Systems, M. Butler and C.B. Jones and A. Romanovski (Ed.), , Springer  (2006)

McIver:05b

Abstraction and Refinement of Probabilistic Systems
A. K. McIver and C. C. Morgan
ACM SIGMetrics Performance Evaluation Review, J.-P. Katoen (Ed.), , ACM  (2005)

Notes, and work in progress

McIver:10a

Compositional closure for Bayes Risk in probabilistic noninterference
A. McIver and L. Meinicke and C. Morgan (2011)
Full version of McIver:10.

Hallerstede:07

Qualitative Probabilistic Modelling in Event-B
S. Hallerstede and T. S. Hoang
in Integrated Formal Methods, (Ed.),
LNCS 4591, Springer  (2007)

Morgan:98a

A Quantified Measure of Security 1: a Relational Model
C. C. Morgan and A. K. McIver (1998)

McIver:98a

A Quantified Measure of Security 2: a Programming Logic
A. K. McIver and C. C. Morgan (1998)

DR96

Probabilistic Data Refinement (1996)

DC96

The Choice-Coordination Problem: Notes for a Correctness Proof (1996)

RW96

Notes on the Random Walk: an Example of Probabilistic Temporal Reasoning (1996)

RDP98

An Example of Probabilistic Variants: The Free Philosophers (1998)

Related work

Halpern:07

Reasoning about Expectation
J. Y. Halpern and R. Pucella
Jnl ACM
To appear.

Keimel:07

Predicate Transformers for Convex Powerdomains
K. Keimel and G. D. Plotkin
Under review.

Varacca:06

Distributing Probability over Non-Determinism
D. Varacca and G. Winskel
Math Struct Comp Sci 16(1):87–113
Cambridge University Press (2006)

Keimel:06

Topological Cones: Foundations for a Domain Theoretical Semantics Combining Probability and Nondeterminism
K. Keimel
155:423–43
Elsevier (2006)

Schneider:06

Tank Monitoring: a pAMN Case Study
S. Schneider, T. S. Hoang, K. A. Robinson, and H. Treharne
Formal Aspects of Computing 18(3):308–28
 (2006)

Tix:09

Semantic Domains for Combining Probability and Non-Determinism
R. Tix, K. Keimel, and G. Plotkin
Electron. Notes Theor. Comput. Sci. 222:3--99
Elsevier (2009)

Tix:05

Semantic Domains for Combining Probability and Non-Determinism
R. Tix, K. Keimel, and G. D. Plotkin
ENTCS 129:1--104
Elsevier (2005)

Huth:04

An Abstraction Framework for Mixed Non-deterministic and Probabilistic Systems
M. Huth
in Validation of Stochastic Systems, C. Baier et al (Ed.), 419–44
LNCS 2925, Springer  (2004)

Zielonka:04

Perfect-Information Stochastic Parity Games
W. Zielonka
in Proc FOSSACS ’04, I. Walukiewicz (Ed.), 499–513
LNCS 2987, Springer (2004)

Schneider:04

Tank Monitoring: a Case Study in pAMN
S. Schneider, T. S. Hoang, K. A. Robinson, and H. Treharne
ENTCS 137(2)
Elsevier (2005)

Fidge:03

But what if I don’t want to wait forever?
C. Fidge and C. Shankland
Formal Aspects of Computing 14(3):281–94
Elsevier (2003)

Ying:03

Reasoning about Probabilistic Sequential Programs in a Probabilistic Logic
M. Ying
Acta Inf 39(5):315–89
Springer (2003)

Butler:99

Reasoning about Grover’s quantum search algorithm using Probabilistic wp
M. J. Butler and P. H. Hartel
ACM Trans Prog Lang Sys 21(3):417–30
ACM (1999)

Huth:97

Quantitative Analysis and Model Checking
M. Huth and M. Kwiatkowska
LICS ’97, 111–22, IEEE (1997)

Sere:96

Probabilities in Action Systems
K. Sere and E. Troubitsyna
Proc 8th Nordic Wkshp Programming Theory, (Ed.), , (1996)

Segala:95b

Modeling and Verification of Randomized Distributed Real-Time Systems
R. Segala
PhD thesis, MIT
(1995)

Hallerstede

Performance Analysis of Probabilistic Action Systems
S. Hallerstede and M. Butler
Under review.

Vasquez

Probabilistic Hoare Logics in Comparison
M. D. Vasquez and N. Wolovick and P. D'Argenio