Carroll's research is on formal methods, semantics, security, program correctness and probability.
Email:  carroll.morgan@unsw.edu.au 

Web:  https:/ 
More contact information is available at the Contact page.
Current 
Past 
Australian Professorial Fellow, UNSW Lecturer/Reader Oxford University UK
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 
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  
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 
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  
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 
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  
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 2030, 2020, Proceedings, Part I, pp. 216–239, 2020 
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:136:50, March, 2019  
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. 3254, 2019  
Annabelle McIver and Carroll Morgan Proving that programs are differentially private Programming Languages and Systems, pp. 3–18, 2019  
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 
Annabelle McIver, Carroll Morgan, Benjamin Kaminski and JoostPieter Katoen A new proof rule for almostsure termination ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, Los Angeles, January, 2018 
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. 112126, October, 2017  
Nicolas Bordenabe, Annabelle McIver, Carroll Morgan and Tahiry Rabehaja Reasoning about distributed secrets FORTE, pp. 156170, Shanghai, June, 2017  
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  
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 
June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan and Christine Rizkallah Proof of OS scheduling behavior in the presence of interruptinduced concurrency International Conference on Interactive Theorem Proving, pp. 52–68, Nancy, France, August, 2016  
Mario Alvim, Kostantinos Chatzikokolakis, Annabelle McIver, Carroll Morgan, Catuscia Palamidessi and Geoffrey Smith Axioms for information leakage Computer Security Foundations, pp. 7792, Lisbon, June, 2016 

June Andronick, Corey Lewis and Carroll Morgan Controlled OwickiGries 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  
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  

Carroll Morgan a nondeterministic lattice of information Onehour invited talk at Mathematics of Program Construction, Königswinter, Germany, June, 2015  
Annabelle McIver, Larissa Meinicke and Carroll Morgan Hiddenmarkov program algebra with iteration Mathematical Structures in Computer Science, Volume 25, Number 2, pp. 320–360, 2015 
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  
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  
Carroll Morgan, Annabelle McIver, Geoffrey Smith, Barbara Espinoza and Larisa Meinicke Abstract channels and their robust informationleakage ordering Principles of Security and Trust (ETAPS), pp. 83–102, Grenoble, France, April, 2014 
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 
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 
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 
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  
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  
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 

Robert Sison Proving confidentiality and its preservation under compilation for mixedsensitivity concurrent programs PhD Thesis, UNSW, October, 2020 