Up to PSG's main page.

This updated bibliography is under construction; the old bibliography is here.

Go to most recent:    McIver:2008yq, Morgan:07, Deng:07, Deng:07a and Cohen:06.
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) 		  Draft Springer bookcover   Draft Springer bookcover

Invited book chapters:

Presentations:

Themes

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

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. C. Morgan, and C. Zhang
LiCS 2007, to appear.
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 Glabeek, 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.
Probability and nondeterminism in sequential programming
McIver:06a
Developing and Reasoning about Probabilistic Programs in pGCL
A. K. McIver and C. C. Morgan
The Pernambuco Formal-Methods Summer School, Ana Cavalcanti and J.C.P. Woodcock and A. Sampaio (Ed.), , Springer  (2006)
He:05
Deriving Probabilistic Semantics via the Weakest Completion
J. He, A. K. McIver, and C. C. Morgan
in Proc IFCEM 04, J. Davies (Ed.),
LNCS 3308, Springer (2005)
McIver:05
An Elementary Proof that Herman’s Ring has Complexity THETA(N-squared)
A. K. McIver and C. C. Morgan
Inf Proc Lett 94(2)
Elsevier (2005)
Yu:03
Generating Distributions
J. Yu
MSc Thesis  Oxford University (2003)
McIver:01a
Demonic, Angelic and Unbounded Probabilistic Choices in Sequential Programs
A. K. McIver and C. C. Morgan
Acta Inf 37(4/5):329–54
Springer (2001)
See also Chapter 8.
McIver:00
Probably Hoare? Hoare Probably!
A. K. McIver, C. C. Morgan, and J. W. Sanders
in Millennial Perspectives in Computer Science, J.W. Davies and A.W. Roscoe and J.C.P. Woodcock (Ed.), 271–82
Cornerstones of Computing , Palgrave  (2000)
See also Chapters 1,2 & Appendix A.
Morgan:99a
pGCL: Formal Reasoning for Random Algorithms
C. C. Morgan and A. K. McIver
South African Comp Jnl 22:14–27
Computer Society of South Africa (1999)
See also Chapter 1&3.
Morgan:98
The Generalised Substitution Language Extended to Probabilistic Programs
C. C. Morgan
in Proc 2nd Int B Conf (B’98), Didier Bert (Ed.), 9–25
LNCS 1393, Springer (1998)
McIver:98
The Probabilistic Steam Boiler: a Case Study in Probabilistic Data Refinement
A. K. McIver, C. C. Morgan, and E. Troubitsyna
in Proc International Refinement Workshop, ANU, Canberra, J. Grundy and M. Schwenke and T. Vickers (Ed.), 250–65
Discrete Mathematics and Computer Science , Springer (1998)
See also Chapter 4.
He:97
Probabilistic Models for the Guarded Command Language
J. He, K. Seidel, and A. McIver
Science of Computer Programming 28:171–92
 (1997)
McIver:97
Partial Correctness for Probabilistic Demonic Programs
A. K. McIver and C. C. Morgan
PRG Technical Report  PRG-TR-35-97  Oxford University (1997)
See also Chapter 7 & Appendices B.2,B.3.
Morgan:96
Unifying wp and wlp
C. C. Morgan and A. K. McIver
Inf Proc Lett 20(3):159–64
Elsevier (1996)
Seidel:96
An Introduction to Probabilistic Predicate Transformers
K. Seidel, C. C. Morgan, and A. K. McIver
PRG Technical Report  PRG-TR-6-96  Oxford University (1996)
Morgan:96d
Probabilistic Predicate Transformers
C. C. Morgan, A. K. McIver, and K. Seidel
ACM Trans Prog Lang Sys 18(3):325–53
ACM (1996)
See also Chapter 5 & Appendix B.5.
Morgan:96b
Proof Rules for Probabilistic Loops
C. C. Morgan
in Proc BCS-FACS 7th Refinement Workshop, He Jifeng and John Cooke and Peter Wallis (Ed.),
Workshops in Computing , Springer (1996)
See also Chapter 2&7, Appendices B.2,B.3.
McIver:96
Probabilistic Predicate Transformers: Part 2
A. K. McIver and C. C. Morgan
PRG Technical Report  PRG-TR-5-96  Oxford University (1996)
See also Appendix B.4.
Stochastic games; quantitative modal- and temporal logic
McIver:07
Results on the Quantitative Mu-Calculus qMu
A. K. McIver and C. C. Morgan
ACM Trans Comp Logic 8(1)
ACM (2007)
See also Chapter 11.
McIver:05c
A Novel Stochastic Game via the quantitative mu-calculus
A. K. McIver and C. C. Morgan
in Proc 3rd QAPL, A. Cerone and A. de Pierro (Ed.),
ENTCS 153, Elsevier (2005)
McIver:05d
Memoryless Strategies for Stochastic Games via Domain Theory
A. K. McIver and C. C. Morgan
in Proc Brazilian Symp Formal Methods, A. Mota (Ed.),
ENTCS 130, Elsevier (2005)
Morgan:03
Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL
C. C. Morgan and A. K. McIver
Theo Comp Sci 293(3):507–34
Elsevier (2003)
McIver:02b
Quantitative Program Logic and Performance in Probabilistic Distributed Algorithms
A. K. McIver
Theo Comp Sci 282(1):191–219
Elsevier (2002)
McIver:02
Games, Probability and the Quantitative mu-Calculus qMu
A. K. McIver and C. C. Morgan
in Proc LPAR, A. Voronkov and M. Boaz (Ed.), 292–310
LNAI 2514, Springer (2002)
See also Chapter 11.
Morgan:01
Cost Analysis of Games Using Program Logic
C. C. Morgan and A. K. McIver
Proc of the 8th Asia-Pacific Software Engineering Conference (APSEC 2001), (Ed.), , IEEE (2001)
Morgan:00
Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL
C. C. Morgan and A. K. McIver
in Proceedings CATS ’01, Colin Fidge (Ed.),
ENTCS 42, Elsevier (2000)
McIver:99a
Reasoning about Efficiency within a Probabilistic mu-calculus
A. K. McIver
in Proc ProbMiv ’98 (LICS), (Ed.),
ENTCS , Elsevier (1999)
Morgan:99
An Expectation-Based Model for Probabilistic Temporal Logic
C. C. Morgan and A. K. McIver
Logic Jnl IGPL 7(6):779–804
Oxford University Press (1999)
See also Chapter 10 & Appendix B.6.
McIver:99
Quantitative Program Logic and Counting Rounds in Probabilistic Distributed Algorithms
A. K. McIver
in Proc 5th Intl Workshop ARTS ’99, (Ed.),
LNCS 1601, Springer (1999)
See McIver:02b.
Morgan:97
A Probabilistic Temporal Calculus Based on Expectations
C. C. Morgan and A. K. McIver
Proc Formal Methods Pacific ’97, (Ed.), 4–22, Springer (1997)
See also Chapter 9 & Appendix B.6, Huth:97.
Information security and anonymity
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 Morgan:98a & McIver:98a.
Quantum computation
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
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
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
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
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,
To appear.
Gonzalia:07
Automating Refinement Checking in Probabilistic System Design
C. Gonzalia and A. K. McIver
Under review.
McIver:07a
Using Probabilistic Kleene Algebra pKA for Protocol Verification
A. K. McIver and C. Gonzalia and E. Cohen and C. C. Morgan
Under review.
Hallerstede:07
Qualitative Probabilistic Modelling in Event-B
S. Hallerstede and T. S. Hoang
Under review.
Morgan:07
The Shadow Knows: Refinement of Ignorance in Sequential Programs
C. C. Morgan
To appear in Sci. Comp. Prog.
See also Morgan:06.
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: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)
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

Return to the top.