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)

Probabilistic Models for the Guarded Command Language. - Jifeng He 001; Karen Seidel 002; Annabelle McIver (Sci. Comput. Program., 1997)

Reasoning about efficiency within a probabilistic µ-calculus. - Annabelle McIver (PROBMIV, 1998)

Quantitative Program Logic and Performance in Probabilistic Distributed Algorithms. - Annabelle McIver (ARTS, 1999)

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

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)

A Generalisation of Stationary Distributions, and Probabilistic Program Algebra. - Annabelle McIver (MFPS, 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)

Quantitative program logic and expected time bounds in probabilistic distributed algorithms. - Annabelle McIver (Theor. Comput. Sci., 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)

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)

Cost-Based Analysis of Probabilistic Programs Mechanised in HOL. - Orieta Celiku; Annabelle McIver (Nord. J. Comput., 2004)

Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs. - Orieta Celiku; Annabelle McIver (FM, 2005)

Towards Automated Proof Support for Probabilistic Distributed Systems. - Annabelle McIver; Tjark Weber (LPAR, 2005)

Development via Refinement in Probabilistic B - Foundation and Case Study. - Thai Son Hoang; Zhendong Jin; Ken Robinson; Annabelle McIver; Carroll Morgan (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)

Quantitative Refinement and Model Checking for the Analysis of Probabilistic Systems. - Annabelle McIver (FM, 2006)

Quantitative µ-Calculus Analysis of Power Management in Wireless Networks. - Annabelle McIver (ICTAC, 2006)

Formal Techniques for the Analysis of Wireless Networks. - A. K. McIver; Ansgar Fehnker (ISoLA, 2006)

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

Automating Refinement Checking in Probabilistic System Design. - Carlos Gonzalía; Annabelle McIver (ICFEM, 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)

CaVi – Simulation and Model Checking for Wireless Sensor Networks. - Athanassios Boulis; Ansgar Fehnker; Matthias Fruth; Annabelle McIver (QEST, 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)

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)

The Secret Art of Computer Programming. - Annabelle McIver (ICTAC, 2009)

Graphical Modelling for Simulation and Formal Analysis of Wireless Network Protocols. - Ansgar Fehnker; Matthias Fruth; Annabelle McIver (Methods, Models and Tools for Fault Tolerance, 2009)

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

YAGA: Automated Analysis of Quantitative Safety Specifications in Probabilistic B. - Ukachukwu Ndukwu; A. K. McIver (ATVA, 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)

An expectation transformer approach to predicate abstraction and data independence for probabilistic programs - Ukachukwu Ndukwu; Annabelle McIver (QAPL, 2010)

Towards an Algebra of Routing Tables. - Peter Höfner; Annabelle McIver (RAMiCS, 2011)

On Probabilistic Kleene Algebras, Automata and Simulations. - Annabelle McIver; Tahiry M. Rabehaja; Georg Struth (RAMiCS, 2011)

Continual and explicit comparison to promote proactive facilitation during second computer language learning. - Matt Bower; Annabelle McIver (ITiCSE, 2011)

Model exploration and analysis for quantitative safety refinement in probabilistic B - Ukachukwu Ndukwu; Annabelle McIver (Refine@FM, 2011)

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

A Process Algebra for Wireless Mesh Networks. - Ansgar Fehnker; Rob J. van Glabbeek; Peter Höfner; Annabelle McIver; Marius Portmann; Wee Lum Tan (ESOP, 2012)

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

A rigorous analysis of AODV and its variants. - Peter Höfner; Rob J. van Glabbeek; Wee Lum Tan; Marius Portmann; Annabelle McIver; Ansgar Fehnker (MSWiM, 2012)

Operational Versus Weakest Precondition Semantics for the Probabilistic Guarded Command Language. - Friedrich Gretz; Joost-Pieter Katoen; Annabelle McIver (QEST, 2012)

Automated Analysis of AODV Using UPPAAL. - Ansgar Fehnker; Rob J. van Glabbeek; Peter Höfner; Annabelle McIver; Marius Portmann; Wee Lum Tan (TACAS, 2012)

Preface: Special Issue QFM 2009. - Suzana Andover; Annabelle McIver; Manuel Núñez 001 (J. Log. Algebraic Methods Program., 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)

An Event Structure Model for Probabilistic Concurrent Kleene Algebra. - Annabelle McIver; Tahiry M. Rabehaja; Georg Struth (LPAR, 2013)

Statistical Model Checking of Wireless Mesh Routing Protocols. - Peter Höfner; Annabelle McIver (NASA Formal Methods, 2013)

Prinsys - On a Quest for Probabilistic Loop Invariants. - Friedrich Gretz; Joost-Pieter Katoen; Annabelle McIver (QEST, 2013)

A Process Algebra for Wireless Mesh Networks used for Modelling, Verifying and Analysing AODV. - Ansgar Fehnker; Rob J. van Glabbeek; Peter Höfner; Annabelle McIver; Marius Portmann; Wee Lum Tan (CoRR, 2013)

Probabilistic Concurrent Kleene Algebra. - Annabelle McIver; Tahiry M. Rabehaja; Georg Struth (QAPL, 2013)

Weak Concurrent Kleene Algebra with Application to Algebraic Verification - Annabelle McIver; Tahiry M. Rabehaja; Georg Struth (CoRR, 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)

Program Refinement, Perfect Secrecy and Information Flow. - Annabelle McIver (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)

Hopscotch - reaching the target hop by hop. - Peter Höfner; Annabelle McIver (J. Log. Algebraic Methods Program., 2014)

Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. - Friedrich Gretz; Joost-Pieter Katoen; Annabelle McIver (Perform. Evaluation, 2014)

Modelling and Analysis of AODV in UPPAAL. - Ansgar Fehnker; Rob J. van Glabbeek; Peter Höfner; Annabelle McIver; Marius Portmann; Wee Lum Tan (CoRR, 2015)

Challenges and Trends in Probabilistic Programming (Dagstuhl Seminar 15181). - Gilles Barthe; Andrew D. Gordon 001; Joost-Pieter Katoen; Annabelle McIver (Dagstuhl Reports, 2015)

Conditioning in Probabilistic Programming. - Nils Jansen 001; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Federico Olmedo; Friedrich Gretz; Annabelle McIver (MFPS, 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)

Schedulers and Finishers: On Generating the Behaviours of an Event Structure. - Annabelle McIver; Tahiry M. Rabehaja; Georg Struth (ICTAC, 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)

Probabilistic rely-guarantee calculus. - Annabelle McIver; Tahiry M. Rabehaja; Georg Struth (Theor. Comput. Sci., 2016)

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

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

Formal Analysis of the Information Leakage of the DC-Nets and Crowds Anonymity Protocols. - Arthur Américo; Artur Vaz; Mário S. Alvim; Sérgio Vale Aguiar Campos; Annabelle McIver (SBMF, 2017)

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

An Algebraic Approach for Reasoning About Information Flow. - Arthur Américo; Mário S. Alvim; Annabelle McIver (FM, 2018)

Processing Text for Privacy: An Information Flow Perspective. - Natasha Fernandes; Mark Dras; Annabelle McIver (FM, 2018)

Author Obfuscation Using Generalised Differential Privacy. - Natasha Fernandes; Mark Dras; Annabelle McIver (CoRR, 2018)

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

Schedulers and finishers: On generating and filtering the behaviours of an event structure. - Annabelle McIver; Tahiry M. Rabehaja; Georg Struth (Theor. Comput. Sci., 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)

Experiments in Information Flow Analysis. - Annabelle McIver (MPC, 2019)

Generalised Differential Privacy for Text Document Processing. - Natasha Fernandes; Mark Dras; Annabelle McIver (POST, 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)

On Privacy and Accuracy in Data Releases (Invited Paper). - Mário S. Alvim; Natasha Fernandes; Annabelle McIver; Gabriel Henrique Nunes (CONCUR, 2020)

Reasoning with Failures. - Hamid Jahanian; Annabelle McIver (ICFEM, 2020)

Failure Mode Reasoning in Model Based Safety Analysis. - Hamid Jahanian; David Parker 002; Marc Zeller; Annabelle McIver; Yiannis Papadopoulos (IMBSA, 2020)

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

Introduction to the Special Section on Quantitative Evaluation of Systems (QEST 2018). - Annabelle McIver; András Horváth (ACM Trans. Model. Perform. Evaluation Comput. Syst., 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)

Editorial. - Annabelle McIver; Maurice H. ter Beek (Formal Aspects Comput., 2021)

Formal methods: practical applications and foundations. - Maurice H. ter Beek; Annabelle McIver (Formal Methods Syst. Des., 2021)

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

Explaining epsilon in differential privacy through the lens of information theory. - Natasha Fernandes; Annabelle McIver; Parastoo Sadeghi (CoRR, 2022)

Directional Privacy for Deep Learning. - Pedro Faustini; Natasha Fernandes; Annabelle McIver; Mark Dras (CoRR, 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)

A Quantitative Information Flow Analysis of the Topics API. - Mário S. Alvim; Natasha Fernandes; Annabelle McIver; Gabriel Henrique Nunes (WPES@CCS, 2023)

Universal optimality and robust utility bounds for metric differential privacy. - Natasha Fernandes; Annabelle McIver; Catuscia Palamidessi; Ming Ding 001 (J. Comput. Secur., 2023)

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

The Privacy-Utility Trade-off in the Topics API. - Mário S. Alvim; Natasha Fernandes; Annabelle McIver; Gabriel H. Nunes (CCS, 2024)

Explaining ∊ in Local Differential Privacy Through the Lens of Quantitative Information Flow. - Natasha Fernandes; Annabelle McIver; Parastoo Sadeghi (CSF, 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)

Bayes' capacity as a measure for reconstruction attacks in federated learning. - Sayan Biswas; Mark Dras; Pedro Faustini; Natasha Fernandes; Annabelle McIver; Catuscia Palamidessi; Parastoo Sadeghi (CoRR, 2024)

IDT: Dual-Task Adversarial Attacks for Privacy Protection. - Pedro Faustini; Shakila Mahjabin Tonni; Annabelle McIver; Qiongkai Xu; Mark Dras (CoRR, 2024)

Comparing privacy notions for protection against reconstruction attacks in machine learning. - Sayan Biswas; Mark Dras; Pedro Faustini; Natasha Fernandes; Annabelle McIver; Catuscia Palamidessi; Parastoo Sadeghi (CoRR, 2025)

Empirical Calibration and Metric Differential Privacy in Language Models. - Pedro Faustini; Natasha Fernandes; Annabelle McIver; Mark Dras (CoRR, 2025)

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