Carroll Morgan

117 papers A* 5A 3B 10C 6Journal 55Unranked 30

Year	Rank	Type	Title / Venue / Authors
2025	C	`conf`	Forward and Backward Simulations for Partially Observable Probability. ICTAC Chris Chen, Annabelle McIver, Carroll Morgan
2025	J	`jnl`	Forward and Backward Simulations for Partially Observable Probability. CoRR Chris Chen, Annabelle McIver, Carroll Morgan
2025	J	`jnl`	On Formal Methods Thinking in Computer Science Education. Formal Aspects Comput. Brijesh Dongol, Catherine Dubois, Stefan Hallerstede, Eric C. R. Hehner, Carroll Morgan, Peter Müller, Leila Ribeiro, Alexandra Silva, Graeme Smith, Erik P. de Vink
2024	C	`conf`	Probabilistic Datatypes. ICTAC Chris Chen, Annabelle McIver, Carroll Morgan
2024	—	`conf`	Source-Level Reasoning for Quantifying Information Leaks. Principles of Verification (1) Chris Chen, Annabelle McIver, Carroll Morgan
2024	J	`jnl`	Source-level reasoning for quantitative information flow. CoRR Chris Chen, Annabelle McIver, Carroll Morgan
2023	A*	`conf`	A Novel Analysis of Utility in Privacy Pipelines, Using Kronecker Products and Quantitative Information Flow. CCS Mário S. Alvim, Natasha Fernandes, Annabelle McIver, Carroll Morgan, Gabriel Henrique Nunes
2023	J	`jnl`	A novel analysis of utility in privacy pipelines, using Kronecker products and quantitative information flow. CoRR Mário S. Alvim, Natasha Fernandes, Annabelle McIver, Carroll Morgan, Gabriel Henrique Nunes
2022	J	`jnl`	Flexible and scalable privacy assessment for very large datasets, with an application to official governmental microdata. CoRR Mário S. Alvim, Natasha Fernandes, Annabelle McIver, Carroll Morgan, Gabriel Henrique Nunes
2022	J	`jnl`	Flexible and scalable privacy assessment for very large datasets, with an application to official governmental microdata. Proc. Priv. Enhancing Technol. Mário S. Alvim, Natasha Fernandes, Annabelle McIver, Carroll Morgan, Gabriel Henrique Nunes
2022	B	`conf`	How to Develop an Intuition for Risk... and Other Invisible Phenomena (Invited Talk). CSL Natasha Fernandes, Annabelle McIver, Carroll Morgan
2021	—	`ch.`	Algorithmics. IFIP's Exciting First 60+ Years 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
2021	A*	`conf`	The Laplace Mechanism has optimal utility for differential privacy over continuous queries. LICS Natasha Fernandes, Annabelle McIver, Carroll Morgan
2021	J	`jnl`	The Laplace Mechanism has optimal utility for differential privacy over continuous queries. CoRR Natasha Fernandes, Annabelle McIver, Carroll Morgan
2020	—	`conf`	Correctness by Construction for Probabilistic Programs. ISoLA (1) Annabelle McIver, Carroll Morgan
2020	J	`jnl`	Correctness by construction for probabilistic programs. CoRR Annabelle McIver, Carroll Morgan
2020	J	`jnl`	Preface. Acta Informatica Peter Höfner, Carroll Morgan, Vaughan R. Pratt
2020	—	`ch.`	Quantitative Information Flow with Monads in Haskell. Foundations of Probabilistic Programming Jeremy Gibbons, Annabelle McIver, Carroll Morgan, Tom Schrijvers
2020	—	`book`	The Science of Quantitative Information Flow. Mário S. Alvim, Konstantinos Chatzikokolakis, Annabelle McIver, Carroll Morgan, Catuscia Palamidessi, Geoffrey Smith
2019	J	`jnl`	Abstract Hidden Markov Models: a monadic account of quantitative information flow. Log. Methods Comput. Sci. Annabelle McIver, Carroll Morgan, Tahiry M. Rabehaja
2019	J	`jnl`	An axiomatization of information flow measures. Theor. Comput. Sci. Mário S. Alvim, Konstantinos Chatzikokolakis, Annabelle McIver, Carroll Morgan, Catuscia Palamidessi, Geoffrey Smith
2019	—	`conf`	Categorical Information Flow. The Art of Modelling Computational Systems Tahiry M. Rabehaja, Annabelle McIver, Carroll Morgan, Georg Struth
2019	B	`conf`	Proving that Programs Are Differentially Private. APLAS Annabelle McIver, Carroll Morgan
2018	J	`jnl`	A new proof rule for almost-sure termination. Proc. ACM Program. Lang. Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, Joost-Pieter Katoen
2017	—	`conf`	A Demonic Lattice of Information. Concurrency, Security, and Puzzles Carroll Morgan
2017	J	`jnl`	A New Proof Rule for Almost-Sure Termination. CoRR Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, Joost-Pieter Katoen
2017	J	`jnl`	Abstract Hidden Markov Models: a monadic account of quantitative information flow. CoRR Annabelle McIver, Carroll Morgan, Tahiry M. Rabehaja
2017	J	`jnl`	Privacy in elections: How small is "small"? J. Inf. Secur. Appl. Annabelle McIver, Tahiry M. Rabehaja, Roland Wen, Carroll Morgan
2017	C	`conf`	Reasoning About Distributed Secrets. FORTE Nicolás E. Bordenabe, Annabelle McIver, Carroll Morgan, Tahiry M. Rabehaja
2016	J	`jnl`	A new rule for almost-certain termination of probabilistic and demonic programs. CoRR Annabelle McIver, Carroll Morgan
2016	A	`conf`	Axioms for Information Leakage. CSF Mário S. Alvim, Konstantinos Chatzikokolakis, Annabelle McIver, Carroll Morgan, Catuscia Palamidessi, Geoffrey Smith
2016	J	`jnl`	Compositional security and collateral leakage. CoRR Nicolás E. Bordenabe, Annabelle McIver, Carroll Morgan, Tahiry M. Rabehaja
2016	B	`conf`	Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency. ITP June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan, Christine Rizkallah
2015	A*	`conf`	Abstract Hidden Markov Models: A Monadic Account of Quantitative Information Flow. LICS Annabelle McIver, Carroll Morgan, Tahiry M. Rabehaja
2015	—	`conf`	Controlled Owicki-Gries Concurrency: Reasoning about the Preemptible eChronos Embedded Operating System. MARS June Andronick, Corey Lewis, Carroll Morgan
2015	J	`jnl`	Hidden-Markov program algebra with iteration. Math. Struct. Comput. Sci. Annabelle McIver, Larissa Meinicke, Carroll Morgan
2014	—	`conf`	(In-)Formal Methods: The Lost Art - A Users' Manual. SETSS Carroll Morgan
2014	—	`conf`	Abstract Channels and Their Robust Information-Leakage Ordering. POST Annabelle McIver, Carroll Morgan, Geoffrey Smith, Barbara Espinoza, Larissa Meinicke
2014	A	`conf`	Additive and Multiplicative Notions of Leakage, and Their Capacities. CSF Mário S. Alvim, Konstantinos Chatzikokolakis, Annabelle McIver, Carroll Morgan, Catuscia Palamidessi, Geoffrey Smith
2014	J	`jnl`	An old new notation for elementary probability theory. Sci. Comput. Program. Carroll Morgan
2014	J	`jnl`	Real-reward testing for probabilistic processes. Theor. Comput. Sci. Yuxin Deng, Rob J. van Glabbeek, Matthew Hennessy, Carroll Morgan
2014	J	`jnl`	Selected papers from the Brazilian Symposium on Formal Methods (SBMF 2011). Sci. Comput. Program. Adenilso da Silva Simão, Carroll Morgan
2014	B	`conf`	Towards a Formal Analysis of Information Leakage for Signature Attacks in Preferential Elections. FM Roland Wen, Annabelle McIver, Carroll Morgan
2012	A*	`conf`	A Kantorovich-Monadic Powerdomain for Information Hiding, with Probability and Nondeterminism. LICS Annabelle McIver, Larissa Meinicke, Carroll Morgan
2012	J	`jnl`	Compositional noninterference from first principles. Formal Aspects Comput. Carroll Morgan
2012	B	`conf`	Elementary Probability Theory in the Eindhoven Style. MPC Carroll Morgan
2012	J	`jnl`	Quantitative methods in security and safety critical applications (NII Shonan Meeting 2012-10). NII Shonan Meet. Rep. Jin Song Dong, Annabelle McIver, Carroll Morgan
2011	—	`ed.`	Formal Methods, Foundations and Applications - 14th Brazilian Symposium, SBMF 2011, São Paulo, Brazil, September 26-30, 2011, Revised Selected Papers SBMF Adenilso da Silva Simão, Carroll Morgan
2011	J	`jnl`	Hidden-Markov Program Algebra with iteration CoRR Annabelle McIver, Larissa Meinicke, Carroll Morgan
2011	—	`conf`	Real-Reward Testing for Probabilistic Processes (Extended Abstract) QAPL Yuxin Deng, Rob J. van Glabbeek, Matthew Hennessy, Carroll Morgan
2010	—	`conf`	Compositional Closure for Bayes Risk in Probabilistic Noninterference. ICALP (2) Annabelle McIver, Larissa Meinicke, Carroll Morgan
2010	J	`jnl`	Compositional closure for Bayes Risk in probabilistic noninterference CoRR Annabelle McIver, Larissa Meinicke, Carroll Morgan
2009	—	`conf`	How to Brew-up a Refinement Ordering. REFINE@FMWeek Carroll Morgan
2009	—	`ed.`	Proceedings First Workshop on Quantitative Formal Methods: Theory and Applications, QFM 2009, Eindhoven, The Netherlands, 3rd November 2009. QFM Suzana Andova, Annabelle McIver, Pedro R. D'Argenio, Pieter J. L. Cuijpers, Jasen Markovski, Carroll Morgan, Manuel Núñez
2009	B	`conf`	Security, Probability and Nearly Fair Coins in the Cryptographers' Café. FM Annabelle McIver, Larissa Meinicke, Carroll Morgan
2009	B	`conf`	Testing Finitary Probabilistic Processes. CONCUR Yuxin Deng, Rob J. van Glabbeek, Matthew Hennessy, Carroll Morgan
2009	J	`jnl`	The Shadow Knows: Refinement and security in sequential programs. Sci. Comput. Program. Carroll Morgan
2009	C	`ed.`	Theoretical Aspects of Computing - ICTAC 2009, 6th International Colloquium, Kuala Lumpur, Malaysia, August 16-20, 2009. Proceedings ICTAC Martin Leucker, Carroll Morgan
2008	J	`jnl`	Characterising Testing Preorders for Finite Probabilistic Processes CoRR Yuxin Deng, Matthew Hennessy, Rob J. van Glabbeek, Carroll Morgan
2008	J	`jnl`	Characterising Testing Preorders for Finite Probabilistic Processes. Log. Methods Comput. Sci. Yuxin Deng, Rob J. van Glabbeek, Matthew Hennessy, Carroll Morgan
2007	A*	`conf`	Characterising Testing Preorders for Finite Probabilistic Processes. LICS Yuxin Deng, Rob J. van Glabbeek, Matthew Hennessy, Carroll Morgan, Chenyi Zhang
2007	—	`conf`	Remarks on Testing Probabilistic Processes. Computation, Meaning, and Logic Yuxin Deng, Rob J. van Glabbeek, Matthew Hennessy, Carroll Morgan, Chenyi Zhang
2007	J	`jnl`	Results on the quantitative µ-calculus qMµ. ACM Trans. Comput. Log. Annabelle McIver, Carroll Morgan
2007	A	`conf`	Scalar Outcomes Suffice for Finitary Probabilistic Testing. ESOP Yuxin Deng, Rob J. van Glabbeek, Carroll Morgan, Chenyi Zhang
2006	—	`conf`	Programming-Logic Analysis of Fault Tolerance: Expected Performance of Self-stabilisation. RODIN Book Carroll Morgan, Annabelle McIver
2006	—	`conf`	Using Probabilistic Kleene Algebra for Protocol Verification. RelMiCS Annabelle McIver, Ernie Cohen, Carroll Morgan
2005	—	`conf`	A Novel Stochastic Game Via the Quantitative QAPL Annabelle McIver, Carroll Morgan
2005	J	`jnl`	Abstraction and refinement in probabilistic systems. SIGMETRICS Perform. Evaluation Rev. Annabelle McIver, Carroll Morgan
2005	—	`book`	Abstraction, Refinement and Proof for Probabilistic Systems Annabelle McIver, Carroll Morgan
2005	J	`jnl`	An elementary proof that Herman's Ring is Theta (N Inf. Process. Lett. Annabelle McIver, Carroll Morgan
2005	—	`conf`	Development via Refinement in Probabilistic B - Foundation and Case Study. ZB Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, Carroll Morgan
2005	J	`jnl`	Probabilistic guarded commands mechanized in Theor. Comput. Sci. Joe Hurd, Annabelle McIver, Carroll Morgan
2005	—	`conf`	The Challenge of Probabilistic ZB Carroll Morgan, Thai Son Hoang, Jean-Raymond Abrial
2004	C	`conf`	Deriving Probabilistic Semantics Via the 'Weakest Completion'. ICFEM Jifeng He, Carroll Morgan, Annabelle McIver
2004	—	`conf`	Developing and Reasoning About Probabilistic Programs in PSSE Annabelle McIver, Carroll Morgan
2004	—	`conf`	Memoryless Strategies for Stochastic Games via Domain Theory. SBMF Carroll Morgan, Annabelle McIver
2004	—	`conf`	Of Probabilistic Wp and SP-and Compositionality. 25 Years Communicating Sequential Processes Carroll Morgan
2004	—	`conf`	Probabilistic Guarded Commands Mechanized in QAPL Joe Hurd, Annabelle McIver, Carroll Morgan
2003	J	`jnl`	Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL. Theor. Comput. Sci. Annabelle McIver, Carroll Morgan
2003	—	`conf`	Probabilistic Invariants for Probabilistic Machines. ZB Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, Carroll Morgan
2003	—	`conf`	Probabilistic Termination in B. ZB Annabelle McIver, Carroll Morgan, Thai Son Hoang
2003	J	`jnl`	Results on the quantitative mu-calculus qMu CoRR Annabelle McIver, Carroll Morgan
2002	B	`conf`	Games, Probability and the Quantitative µ-Calculus qMµ. LPAR Annabelle McIver, Carroll Morgan
2001	—	`conf`	Almost-Certain Eventualities and Abstract Probabilities in the Temporal Logic PTL. CATS Annabelle McIver, Carroll Morgan
2001	C	`conf`	Cost Analysis of Games, Using Program Logic. APSEC Carroll Morgan, Annabelle McIver
2001	J	`jnl`	Demonic, angelic and unbounded probabilistic choices in sequential programs. Acta Informatica Annabelle McIver, Carroll Morgan
2001	J	`jnl`	Partial correctness for probabilistic demonic programs. Theor. Comput. Sci. Annabelle McIver, Carroll Morgan
2000	—	`conf`	An Iterator Construct for the Refinement Calculus. IWFM Steve King, Carroll Morgan
1999	J	`jnl`	An Expectation-Transformer Model for Probabilistic Temporal Logic. Log. J. IGPL Carroll Morgan, Annabelle McIver
1998	—	`conf`	The Generalised Substitution Language Extended to Probabilistic Programs. B Carroll Morgan
1996	J	`jnl`	Probabilistic Predicate Transformers. ACM Trans. Program. Lang. Syst. Carroll Morgan, Annabelle McIver, Karen Seidel
1996	J	`jnl`	Refinement-Oriented Probability for CSP. Formal Aspects Comput. Carroll Morgan, Annabelle McIver, Karen Seidel, Jeff W. Sanders
1996	J	`jnl`	Unifying wp and wlp. Inf. Process. Lett. Carroll Morgan, Annabelle McIver
1995	J	`jnl`	Action Systemes, Unbounded Nondeterminism, and Infinite Traces. Formal Aspects Comput. Michael J. Butler, Carroll Morgan
1995	J	`jnl`	Exits in the Refinement Calculus. Formal Aspects Comput. Steve King, Carroll Morgan
1994	J	`jnl`	Foreword: Special Issue on Mathematics of Program Construction. Sci. Comput. Program. Carroll Morgan
1994	—	`book`	Programming from specifications, 2nd Edition. Carroll Morgan
1993	J	`jnl`	A Single Complete Rule for Data Refinement. Formal Aspects Comput. Paul H. B. Gardiner, Carroll Morgan
1993	B	`ed.`	Mathematics of Program Construction, Second International Conference, Oxford, UK, June 29 - July 3, 1992, Proceedings MPC Richard S. Bird, Carroll Morgan, Jim Woodcock
1993	—	`conf`	The Refinement Calculus, and Literate Development. Formal Program Development Carroll Morgan
1992	—	`conf`	The Refinement Calculus. NATO ASI PDC Carroll Morgan
1991	J	`jnl`	Data Refinement of Predicate Transformers. Theor. Comput. Sci. Paul H. B. Gardiner, Carroll Morgan
1990	J	`jnl`	Data Refinement by Calculation. Acta Informatica Carroll Morgan, Paul H. B. Gardiner
1990	—	`book`	Programming from specifications. Carroll Morgan
1990	—	`conf`	Refinement of State-Based Concurrent Systems. VDM Europe Jim Woodcock, Carroll Morgan
1990	J	`jnl`	Types and Invariants in the Refinement Calculus. Sci. Comput. Program. Carroll Morgan, Trevor Vickers
1989	B	`conf`	Types and Invariants in the Refinement Calculus. MPC Carroll Morgan
1988	J	`jnl`	Auxiliary Variables in Data Refinement. Inf. Process. Lett. Carroll Morgan
1988	J	`jnl`	Data Refinement by Miracles. Inf. Process. Lett. Carroll Morgan
1988	J	`jnl`	Procedures, parameters, and abstraction: Separate concerns. Sci. Comput. Program. Carroll Morgan
1988	J	`jnl`	The Specification Statement. ACM Trans. Program. Lang. Syst. Carroll Morgan
1987	J	`jnl`	Laws of Programming. Commun. ACM C. A. R. Hoare, Ian J. Hayes, Jifeng He, Carroll Morgan, A. W. Roscoe, Jeff W. Sanders, Ib Holm Sørensen, J. Michael Spivey, Bernard Sufrin
1985	J	`jnl`	Global and Logical Time in Distributed Algorithms. Inf. Process. Lett. Carroll Morgan
1984	J	`jnl`	Specification of the UNIX Filing System. IEEE Trans. Software Eng. Carroll Morgan, Bernard Sufrin
1983	—	`conf`	Specification of a simplified Network Service in CSP. The Analysis of Concurrent Systems Carroll Morgan, C. A. R. Hoare
1983	—	`conf`	Specification of a simplified Network Service in Z. The Analysis of Concurrent Systems Carroll Morgan
1976	J	`jnl`	A prime decomposition result for parallel systems. SIGACT News Carroll Morgan