Trustworthy Systems

Carroll Morgan
Professor

Research Interests

Carroll's research is on formal methods, semantics, security, program correctness and probability.

Contact Details

Email:carroll.morgan@unsw.edu.au
Web:https://www.unsw.edu.au/staff/carroll-morgan

More contact information is available at the Contact page.

Photo of Carroll Morgan

Publication List

Projects

Current

Past

Career Summary

Australian Professorial Fellow, UNSW Lecturer/Reader Oxford University UK

Publications

Best Papers

Abstract PDF Carroll Morgan, Mário Alvim, Konstantinos Chatzikokolakis, Annabelle McIver, Catuscia Palamidessi and Geoffrey Smith
Additive and multiplicative notions of leakage, and their capacities
Computer Security Foundations, pp. 308–322, Vienna, Austria, July, 2014
Winner of the 2015 NSA Best Scientific Cybersecurity Paper Award


Trustworthy Systems Group Papers

2022

Abstract PDF Mário Alvim, Natasha Fernandes, Annabelle McIver, Carroll Morgan and Gabriel Nunes
Flexible and scalable privacy assessment for very large datasets, with an application to official governmental microdata
Proc. Priv. Enhancing Technol. 2022(4), pp. 378–99, 2022
Abstract PDF Natasha Fernandes, Annabelle McIver and Carroll Morgan
How to develop an intuition for risk... and other invisible phenomena (invited talk)
Proc. Computer Science Logic 2022, pp. 2:1–2:14, 2022

2021

Abstract PDF Richard S. Bird, Jeremy Gibbons, Ralf Hinze, Peter Hoefner, Johan Jeuring, Lambert G. L. T. Meertens, Bernhard Möller, Carroll Morgan, Tom Schrijvers, Wouter Swierstra and Nicolas Wu
Algorithmics
Volume 600 in IFIP Advances in Information and Communication Technology. Springer, 2021
Abstract PDF Natasha Fernandes, Annabelle McIver and Carroll Morgan
The Laplace mechanism has optimal utility for differential privacy over continuous queries
36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2021

2020

Abstract PDF Jeremy Gibbons, Annabelle McIver, Carroll Morgan and Tom Schrijvers
Quantitative information flow with monads in Haskell
Foundations of Probabilistic Programming, pp. 391–448, Cambridge University Press, 2020
Abstract PDF Annabelle McIver and Carroll Morgan
Correctness by construction for probabilistic programs
Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles—9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part I, pp. 216–239, 2020

2019

Abstract PDF Carroll Morgan, Annabelle McIver and Tahiry Rabehaja
Abstract hidden markov models: A monadic account of quantitative information flow
Mathematical Structures in Computer Science, Volume 15, Issue 1, pp. 36:1-36:50, March, 2019
Abstract PDF Mário S. Alvim, Konstantinos Chatzikokolakis, Annabelle McIver, Carroll Morgan, Catuscia Palamidessi and Geoffrey Smith
An axiomatization of information flow measures
Theoretical Computer Science, Volume 777, pp. 32-54, 2019
Abstract PDF Annabelle McIver and Carroll Morgan
Proving that programs are differentially private
Programming Languages and Systems, pp. 3–18, 2019
Abstract PDF Tahiry Rabehaja, Annabelle McIver, Carroll Morgan and Georg Struth
Categorical information flow
The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy: Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday, pp. 329–343, Springer International Publishing, 2019

2018

Abstract PDF Annabelle McIver, Carroll Morgan, Benjamin Kaminski and Joost-Pieter Katoen
A new proof rule for almost-sure termination
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angeles, January, 2018

2017

Abstract PDF Annabelle McIver, Tahiry Rabehaja, Roland Wen and Carroll Morgan
Privacy in elections: How small is "small"?
Journal of Information Security and Applications, Volume 36, Issue 1, pp. 112-126, October, 2017
Abstract PDF Nicolas Bordenabe, Annabelle McIver, Carroll Morgan and Tahiry Rabehaja
Reasoning about distributed secrets
FORTE, pp. 156-170, Shanghai, June, 2017
Abstract PDF Annabelle McIver, Carroll Morgan and Tahiry Rabehaja
Algebra for quantitative information flow
International Conference on Relational and Algebraic Methods in Computer Science, pp. 3–23, Lyon, France, May, 2017
Abstract PDF Carroll Morgan
A demonic lattice of information
Concurrency, Security, and Puzzles — Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday, pp. 203–222, Volume 10160 in Lecture Notes in Computer Science, Springer, 2017

2016

Abstract PDF June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan and Christine Rizkallah
Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
International Conference on Interactive Theorem Proving, pp. 52–68, Nancy, France, August, 2016
Abstract PDF Mario Alvim, Kostantinos Chatzikokolakis, Annabelle McIver, Carroll Morgan, Catuscia Palamidessi and Geoffrey Smith
Axioms for information leakage
Computer Security Foundations, pp. 77-92, Lisbon, June, 2016

2015

Abstract
Slides
PDF June Andronick, Corey Lewis and Carroll Morgan
Controlled Owicki-Gries concurrency: reasoning about the preemptible eChronos embedded operating system
Workshop on Models for Formal Analysis of Real Systems (MARS 2015), pp. 10–24, Suva, Fiji, November, 2015
Abstract PDF Carroll Morgan, Annabelle McIver and Tahiry Rabehaja
Abstract hidden Markov models: A monadic account of quantitative information flow
Annual IEEE Symposium on Logic in Computer Science, pp. 597–608, Tokyo, Japan, July, 2015
Abstract
Slides
PDF Carroll Morgan
a nondeterministic lattice of information
One-hour invited talk at Mathematics of Program Construction, Königswinter, Germany, June, 2015
plain text to be published Annabelle McIver, Larissa Meinicke and Carroll Morgan
Hidden-markov program algebra with iteration
Mathematical Structures in Computer Science, Volume 25, Number 2, pp. 320–360, 2015

2014

Abstract PDF Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan
Real reward testing for probabilistic processes
Theoretical Computer Science, Volume 538, pp. 16–36, July, 2014
Abstract PDF Carroll Morgan, Mário Alvim, Konstantinos Chatzikokolakis, Annabelle McIver, Catuscia Palamidessi and Geoffrey Smith
Additive and multiplicative notions of leakage, and their capacities
Computer Security Foundations, pp. 308–322, Vienna, Austria, July, 2014
Winner of the 2015 NSA Best Scientific Cybersecurity Paper Award
Abstract PDF Carroll Morgan, Annabelle McIver, Geoffrey Smith, Barbara Espinoza and Larisa Meinicke
Abstract channels and their robust information-leakage ordering
Principles of Security and Trust (ETAPS), pp. 83–102, Grenoble, France, April, 2014

2011

Abstract PDF Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan
Real reward testing for probabilistic processes (extended abstract)
Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL 2011), pp. 61–73, Saarbrücken, Germany, July, 2011

2009

Abstract PDF Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan
Testing finitary probabilistic processes (extended abstract)
Proceedings of the 20th International Conference on Concurrency Theory (CONCUR), pp. 274–288, Bologna, Italy, August, 2009

2008

Abstract PDF Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan
Characterising testing preorders for finite probabilistic processes
Logical Methods in Computer Science, Volume 4, Number 4, pp. 1–33, October, 2008

2007

Abstract PDF Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, Carroll Morgan and Cuicui Zhang
Characterising testing preorders for finite probabilistic processes
Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, pp. 313–322, Wroclaw, Poland, July, 2007
Abstract PDF Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, Carroll Morgan and Cuicui Zhang
Remarks on testing probabilistic processes
Electronic Notes in Theoretical Computer Science, Volume 172, Number , pp. 359–397, April, 2007
Abstract PDF Yuxin Deng, Rob van Glabbeek, Carroll Morgan and Chenyi Zhang
Scalar outcomes suffice for finitary probabilistic testing
Proceedings of the 16thEuropean Symposium on Programming, pp. 363–378, Braga, Portugal, March, 2007

Research Theses Supervised

2020

Abstract
Slides
PDF Robert Sison
Proving confidentiality and its preservation under compilation for mixed-sensitivity concurrent programs
PhD Thesis, UNSW, October, 2020