Select Publications

Conference Papers

Andronick J; Lewis C; Morgan C, 2015, 'Controlled owicki-gries concurrency: Reasoning about the preemptible eChronos embedded operating system', in Electronic Proceedings in Theoretical Computer Science, EPTCS, pp. 10 - 24, http://dx.doi.org/10.4204/EPTCS.196.2

McIver A; Morgan C; Rabehaja T, 2015, 'Abstract hidden markov models: A monadic account of quantitative information flow', in Proceedings - Symposium on Logic in Computer Science, pp. 597 - 608, http://dx.doi.org/10.1109/LICS.2015.61

Morgan C, 2015, 'A nondeterministic lattice of information', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 9 - 10

Alvim MS; Chatzikokolakis K; McIver A; Morgan C; Palamidessi C; Smith G, 2014, 'Additive and multiplicative notions of leakage, and their capacities', in Proceedings of the Computer Security Foundations Workshop, pp. 308 - 322, http://dx.doi.org/10.1109/CSF.2014.29

Morgan C, 2014, '(In-)formal methods: The lost art a users’ manual', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Chongqing, China, pp. 1 - 79, presented at First International School, SETSS 2014, Chongqing, China, 08 September 2014 - 13 September 2014, http://dx.doi.org/10.1007/978-3-319-29628-9_1

McIver A; Morgan C; Smith G; Espinoza B; Meinicke L, 2014, 'Abstract channels and their robust information-leakage ordering', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 83 - 102, http://dx.doi.org/10.1007/978-3-642-54792-8_5

Wen R; McIver A; Morgan C, 2014, 'Towards a formal analysis of information leakage for signature attacks in preferential elections', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 595 - 610, http://dx.doi.org/10.1007/978-3-319-06410-9_40

Morgan CC, 2012, 'Elementary probability theory in the Eindhoven style', in 11th International Conference, MPC 2012, Springer, Heidelberg, pp. 48 - 73, presented at Maths of Program Construction, Madrid, 25 June 2012, http://dx.doi.org/10.1007/978-3-642-31113-0_5

McIver A; Meinicke L; Morgan CC, 2012, 'A Kantorovich-monadic powerdomain for information hiding, with probability and nondeterminism', in Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, New Jersey, pp. 461 - 470, presented at Logic in Computer Science, Dubrovnik, http://dx.doi.org/10.1109/LICS.2012.56

Katoen J-P; McIver AK; Meinicke LA; Morgan CC, 2010, 'Linear-Invariant Generation for Probabilistic Programs: Automated Support for Proof-Based Methods', in Cousot R; Martel M (ed.), STATIC ANALYSIS, SPRINGER, FRANCE, Perpignan, pp. 390 - +, presented at 17th International Static Analysis Symposium, FRANCE, Perpignan, 14 September 2010 - 16 September 2010, https://www.webofscience.com/api/gateway?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:000286149800024&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=891bb5ab6ba270e68a29b250adbe88d1

McIver A; Meinicke L; Morgan C, 2010, 'Compositional closure for bayes risk in probabilistic noninterference', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 223 - 235, http://dx.doi.org/10.1007/978-3-642-14162-1_19

McIver A; Meinicke L; Morgan CC, 2010, 'Compositional closure for Bayes Risk in sequential noninterference', in Proceedings ICALP 2010, LNCS 6199, Springer, Bordeaux, pp. 223 - 235, presented at ICALP 2010, Bordeaux, http://portal.acm.org/citation.cfm?id=1880999.1881023

Katoen J; McIver A; Meinicke L; Morgan CC, 2010, 'Linear-invariant generation for probabilistic programs', in AICI - Lecture Notes in Computer Science, Springer, Germany, pp. 390 - 406, presented at SAS 2010, Perpingnan, http://dx.doi.org/10.1007/978-3-642-15769-1_24

Andova S; D'Argenio P; Cuijpers P; McIver A; Markovski J; Morgan C; Núñez M, 2009, 'Preface', in Electronic Proceedings in Theoretical Computer Science, EPTCS, http://dx.doi.org/10.4204/EPTCS.13

McIver A; Meinicke L; Morgan CC, 2009, 'Security, probability and nearly fair coins in the cryptographers' cafe', in Logic Programming, 21st International Conference, Springer, Berlin, presented at Formal Methods 2009, Eindhoven, Netherlands, 02 November 2009 - 06 November 2009, http://dx.doi.org/10.1007/978-3-642-05089-3_5

McIver AK; Morgan CC, 2009, 'Sums and Lovers: Case studies in security, compositionality and refinement', in Logic Programming, 21st International Conference, Springer, Berlin, presented at Formal Methods 2009, Eindhoven, Netherlands, 02 November 2009 - 06 November 2009, http://dx.doi.org/10.1007/978-3-642-05089-3_19

Morgan CC, 2009, 'How to brew-up a refinement order', in Electronic Notes in Theoretical Computer Science, Elsevier BV, Eindhoven, Netherlands, presented at REFINE 2009, Eindhoven, Netherlands, 01 November 2009, http://dx.doi.org/10.1016/j.entcs.2009.12.021

Deng Y; Hennessy M; van Glabbeek RJ; Morgan CC, 2009, 'Testing Finitary Probabilistic Processes', in Proceedings of the First International Conference on Advances in Natural Computation (ICNC 2005), Part III, Lecture Notes in Computer Science 3612/2005, Springer, Berlin, Germany, presented at 20th International Conference on Concurrency Theory, Bologna, Italy, http://dx.doi.org/10.1007/978-3-642-04081-8_19

McIver A; Gonzalia C; Morgan CC, 2008, 'Proofs and refutations for probabilistic systems', in Formal methods 2008, Springer, Turku, Finland, presented at Formal methods 2008, Turku, Finland, 26 May 2008 - 30 May 2008, http://dx.doi.org/10.1007/978-3-540-68237-0_9

McIver AK; Morgan CC; Conzalia C, 2008, 'Proofs and refutations for probabilistic refinement', in Cuellar J; Maibaum T; Sere K (eds.), FM 2008: FORMAL METHODS, PROCEEDINGS, SPRINGER-VERLAG BERLIN, FINLAND, Turku, pp. 100 - +, presented at 15th International Symposium on Formal Methods, FINLAND, Turku, 26 May 2008 - 30 May 2008, https://www.webofscience.com/api/gateway?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:000256247100009&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=891bb5ab6ba270e68a29b250adbe88d1

Deng Y; van Glabbeek RJ; Hennessy M; Morgan CC; Zhang C, 2007, 'Characterising testing preorders for finite probabilistic processes', in 22nd Annual IEEE symposium on logic in computer science, Institute of Electrical and Electronics Engineers Inc., 445 Hoes Lane / P.O. Box 1331, Piscataway, NJ 08855-1331, United States, Wroclaw, Poland, pp. 313 - 322, presented at 22nd Annual IEEE symposium on logic in computer science, Wroclaw, Poland, 10 July 2007 - 14 July 2007, http://dx.doi.org/10.1109/LICS.2007.15

Deng Y; van Glabbeek RJ; Morgan CC; Zhang C, 2007, 'Scalar outcomes suffice for finitary probabilistic testing', in 16th European symposium on programming, 2007, Braga, Portugal, presented at 16th European symposium on programming, 2007, Braga, Portugal, 24 March 2007 - 01 April 2007

McIver A; Cohen EG; Morgan CC, 2006, 'Using Probabilistic Kleene algebra for protocol verification', in Maths of Program Construction, Manchester, England, presented at Maths of Program Construction, Manchester, England, 29 August 2006 - 02 September 2006

Morgan CC, 2006, 'The shadow knows: refinement of ignorance in sequential programs', in Mathematics of program construction, Kurressare, Estonia, presented at Mathematics of program construction, Kurressare, Estonia, 03 July 2006 - 05 July 2006

Hurd J; McIver A; Morgan CC, 2005, 'Probabilistic Guarded Commands Mechanized in HOL', in Electronic Notes in Theoretical Computer Science, Elsevier BV, Barcelona, Spain, presented at Quantitative aspects of programming languages 2005, Barcelona, Spain, 29 November 2005 - 01 December 2005, http://dx.doi.org/10.1016/j.entcs.2004.01.021

Hoang TS; Jin Z; Robinson KA; McIver A; Morgan CC, 2005, 'Development via refinement in probabilistic B - Foundation and case study', in 13th International Conference on FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FoSSaCS 2010), Springer-Verlag, Germany, presented at Formal specification and development in Z and B, Guildford, UK, 13 April 2005 - 15 April 2005, http://dx.doi.org/10.1007/b135596

Morgan CC; McIver A, 2005, 'A novel stochastic game via the quantitative modal mu-calculus', in Electronic Notes in Theoretical Computer Science, Elsevier BV, Edinburgh, Scotland, presented at Quantitative Aspects of Programming Languages 2006, Edinburgh, Scotland, 02 April 2005 - 03 April 2005

Morgan CC; McIver AK, 2005, 'Programming-logic analysis of fault tolerance: Expected performance of self-stabilisation', in Butler M; Jones C; Romanovsky A; Troubitsyna E (eds.), RIGOROUS DEVELOPMENT OF COMPLEX FAULT-TOLERANT SYSTEMS, SPRINGER-VERLAG BERLIN, ENGLAND, Newcastle Univ, Newcastle upon Tyne, pp. 288 - +, presented at Workshop on Rigorous Open Development Environment for Complex Systems, ENGLAND, Newcastle Univ, Newcastle upon Tyne, https://www.webofscience.com/api/gateway?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:000244663400015&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=891bb5ab6ba270e68a29b250adbe88d1

Morgan CC; McIver A; He J, 2004, 'Deriving Probabilistic Semantics vis the Weakest Completion', in 6th International Conference on Formal Engineering Methods, ICFEM 2004, Springer, Seattle, Washington, USA, presented at 6th International Conference on Formal Engineering Methods, ICFEM 2004, Seattle, Washington, USA, 08 November 2004 - 12 November 2004

Morgan CC; McIver A, 2004, 'Memoryless strategies for stochastic games via domain theory', in Electronic Notes in Theoretical Computer Science, Elsevier BV, Recife, presented at Brazilian Symposium on Formal Methods 2004, Recife, http://dx.doi.org/10.1016/j.entcs.2005.03.003

Morgan CC; McIver A; Hoang TS; Robinson KA; Jin Z, 2003, 'Probabilistic invariants for probabilistic machines', in ZB 2003: Formal Specification and develoment in B and Z, Springer, Turku, Finland, presented at ZB 2003: Formal Specification and develoment in B and Z, Turku, Finland, http://dx.doi.org/10.1007/3-540-44880-2_16

Morgan CC; McIver A; Hoang TS, 2003, 'Probabilistic Termination in B', in ZB 2003: Formal Specification and develoment in B and Z, Springer, Turku, Finland, presented at ZB 2003: Formal Specification and develoment in B and Z, Turku, Finland, http://dx.doi.org/10.1007/3-540-44880-2_15

Morgan CC, 2002, 'Games, probability and the quantitative mu-calculus qMu', in Logic for Programming, Artificial Intelligence and Reasoning LNAI 2514, Springer, Tbilisi Georgia, presented at Logic for Programming, Artificial Intelligence and Reasoning, Tbilisi Georgia, 14 October 2002 - 18 October 2002, http://dx.doi.org/10.1007/3-540-36078-6_20

Morgan C, 1998, 'The generalised substitution language extended to probabilistie programs', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 9 - 25, http://dx.doi.org/10.1007/bfb0053351

Woodcock JCP; Morgan C, 1990, 'Refinement of state-based concurrent systems', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 340 - 351, http://dx.doi.org/10.1007/3-540-52513-0_18

Morgan C, 1989, 'Types and invariants in the refinement calculus', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 363 - 378, http://dx.doi.org/10.1007/3-540-51305-1_22

Morgan C; Hoare CAR, 1985, 'Specification of a simplified network service in CSP (Problem 2)', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 345 - 353, http://dx.doi.org/10.1007/3-540-16047-7_56

Morgan C, 1985, 'Specification of a simplified network service in Z (Problem 2)', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 318 - 344, http://dx.doi.org/10.1007/3-540-16047-7_55

Preprints

Alvim MS; Fernandes N; McIver A; Morgan C; Nunes GH, 2023, A novel analysis of utility in privacy pipelines, using Kronecker products and quantitative information flow, , http://dx.doi.org/10.48550/arxiv.2308.11110

Alvim MS; Fernandes N; McIver A; Morgan C; Nunes GH, 2022, Flexible and scalable privacy assessment for very large datasets, with an application to official governmental microdata, , http://dx.doi.org/10.48550/arxiv.2204.13734

Fernandes N; McIver A; Morgan C, 2021, The Laplace Mechanism has optimal utility for differential privacy over continuous queries, , http://dx.doi.org/10.48550/arxiv.2105.07176

McIver A; Morgan C; Kaminski BL; Katoen J-P, 2017, A New Proof Rule for Almost-Sure Termination, , http://dx.doi.org/10.48550/arxiv.1711.03588

McIver A; Morgan C; Rabehaja T, 2017, Abstract Hidden Markov Models: a monadic account of quantitative information flow, , http://dx.doi.org/10.48550/arxiv.1708.01688

Bordenabe N; McIver A; Morgan C; Rabehaja T, 2016, Compositional security and collateral leakage, , http://dx.doi.org/10.48550/arxiv.1604.04983

Andronick J; Lewis C; Morgan C, 2015, Controlled Owicki-Gries Concurrency: Reasoning about the Preemptible eChronos Embedded Operating System, , http://dx.doi.org/10.48550/arxiv.1511.04170

Deng Y; van Glabbeek R; Hennessy M; Morgan C, 2011, Real-Reward Testing for Probabilistic Processes (Extended Abstract), , http://dx.doi.org/10.48550/arxiv.1107.1201

McIver A; Meinicke L; Morgan C, 2011, Hidden-Markov Program Algebra with iteration, , http://dx.doi.org/10.48550/arxiv.1102.0333

McIver A; Meinicke L; Morgan C, 2010, Compositional closure for Bayes Risk in probabilistic noninterference, , http://dx.doi.org/10.48550/arxiv.1007.1054


Back to profile page