Professor Alice Miller

  • Professor (Computing Science)

telephone: 01413304454
email: Alice.Miller@glasgow.ac.uk

Room S133, Computing Science, 13 Lilybank Gardens, Glasgow G12 8QQ

Import to contacts

ORCID iDhttps://orcid.org/0000-0002-0941-1717

Biography

I am a Professor of Computing Science and have worked in the School since 1997, as a Post doc, Daphne Jackson Fellow, Lecturer and Senior Lecturer. Before that I worked in the Universities of East Anglia, Western Australia and Stirling.

My PhD is in Number Theory, but I have worked in Formal Verification for most of my research career. Basically I use mathematical techniques to try to prove things about systems - in particular to try to reduce hard problems to tractable ones.

I am a member of the London Mathematical Society and the IET, and am a Chartered Engineer.

I am currently a Leverhulme research fellow. 

Research interests

Personal site

Formal Verification and Model checking

 

Research Interests:
My research involves using mathematical techniques to analyse complex software systems. These systems include autonomous vehicles (such as UAVs), robots, and telecommunications systems. We develop models which we can analyse using logical properties to define the sort of behaviour we expect the system to have. This allows us to expose hidden errors that could affect the performance, efficiency and sometimes safety of a system. The particular technique I use is a type of formal verification called model checking.

Specifically my research interests include:

- Modelling and Verification
- Abstraction and Symmetry Reduction
- Combinatorics
- Group Theory
- Graph Theory

Publications

Selected publications

Chandler, Christopher ORCID logoORCID: https://orcid.org/0000-0001-5025-1498, Porr, Bernd ORCID logoORCID: https://orcid.org/0000-0001-8157-998X, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Lafratta, Giulia ORCID logoORCID: https://orcid.org/0009-0006-2072-338X (2023) Model Checking for Closed-Loop Robot Reactive Planning. In: Fifth Workshop on Formal Methods for Autonomous Systems (FMAS 2023), Leiden, The Netherlands, 15-16 November 2023, pp. 77-94. (doi: 10.4204/EPTCS.395.6)

Hunter, Ethan T. P. ORCID logoORCID: https://orcid.org/0000-0002-4309-6861, Enright, Jessica ORCID logoORCID: https://orcid.org/0000-0002-0266-3292 and Miller, Alice A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2023) Feasibility assessments of a dynamical approach to compartmental modelling on graphs: scaling limits and performance analysis. Theoretical Computer Science, 980, 114247. (doi: 10.1016/j.tcs.2023.114247)

Davies, Vinny ORCID logoORCID: https://orcid.org/0000-0003-1896-8936, Wandy, Joe ORCID logoORCID: https://orcid.org/0000-0002-3068-4664, Weidt, Stefan, van der Hooft, Justin J.J. ORCID logoORCID: https://orcid.org/0000-0002-9340-5511, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Daly, Rónán ORCID logoORCID: https://orcid.org/0000-0002-1275-6820 and Rogers, Simon ORCID logoORCID: https://orcid.org/0000-0003-3578-4477 (2021) Rapid development of improved data-dependent acquisition strategies. Analytical Chemistry, 93(14), pp. 5676-5683. (doi: 10.1021/acs.analchem.0c03895) (PMID:33784814) (PMCID:PMC8047769)

Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Barr, Matthew ORCID logoORCID: https://orcid.org/0000-0002-5147-0673, Kavanagh, William ORCID logoORCID: https://orcid.org/0000-0003-0521-1643, Valkov, Ivaylo ORCID logoORCID: https://orcid.org/0000-0003-1116-875X and Purchase, Helen C. ORCID logoORCID: https://orcid.org/0000-0001-6994-4446 (2021) Breakout group allocation schedules and the social golfer problem with adjacent group sizes. Symmetry, 13(1), 13. (doi: 10.3390/sym13010013)

Fraser, Douglas, Giaquinta, Ruben, Hoffmann, Ruth, Ireland, Murray, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Norman, Gethin ORCID logoORCID: https://orcid.org/0000-0001-9326-4344 (2020) Collaborative models for autonomous systems controller synthesis. Formal Aspects of Computing, 32, pp. 157-186. (doi: 10.1007/s00165-020-00508-1)

Codish, Michael, Frank, Michael, Itzhakov, Avraham and Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2016) Computing the Ramsey number R(4,3,3) using abstraction and symmetry breaking. Constraints, 21(3), pp. 375-393. (doi: 10.1007/s10601-016-9240-3)

All publications

List by: Type | Date

Jump to: 2025 | 2024 | 2023 | 2022 | 2021 | 2020 | 2019 | 2018 | 2017 | 2016 | 2015 | 2014 | 2013 | 2012 | 2011 | 2010 | 2009 | 2008 | 2007 | 2006 | 2005 | 2004 | 2003 | 2002 | 2001 | 1998 | 1996 | 1994 | 1991
Number of items: 96.

2025

Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Porr, Bernd ORCID logoORCID: https://orcid.org/0000-0001-8157-998X, Valkov, Ivaylo ORCID logoORCID: https://orcid.org/0000-0003-1116-875X, Fraser, Douglas and Pagojus, Daumantas (2025) Model checking with memoisation for fast overtaking planning. Science of Computer Programming, 244, 103300. (doi: 10.1016/j.scico.2025.103300)

Lafratta, Giulia ORCID logoORCID: https://orcid.org/0009-0006-2072-338X, Porr, Bernd ORCID logoORCID: https://orcid.org/0000-0001-8157-998X, Chandler, Christopher ORCID logoORCID: https://orcid.org/0000-0001-5025-1498 and Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2025) Closed-loop multi-step planning. Neural Computation, (Accepted for Publication)

2024

Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Abel, Julian R., Valkov, Ivaylo ORCID logoORCID: https://orcid.org/0000-0003-1116-875X and Fraser, Douglas (2024) Implementing the MOLS table for n up to 500. Symmetry, 16(12), 1678. (doi: 10.3390/sym16121678)

Valkov, Ivaylo ORCID logoORCID: https://orcid.org/0000-0003-1116-875X, Donaldson, Alastair and Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2024) Synchronisation in Language-Level Symmetry Reduction for Probabilistic Model Checking. In: 30th International SPIN symposium on Model Checking of Software (SPIN 2024), Luxembourg, 10-11 Apr 2024, pp. 49-66. ISBN 9783031661488 (doi: 10.1007/978-3-031-66149-5_3)

2023

Chandler, Christopher ORCID logoORCID: https://orcid.org/0000-0001-5025-1498, Porr, Bernd ORCID logoORCID: https://orcid.org/0000-0001-8157-998X, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Lafratta, Giulia ORCID logoORCID: https://orcid.org/0009-0006-2072-338X (2023) Model Checking for Closed-Loop Robot Reactive Planning. In: Fifth Workshop on Formal Methods for Autonomous Systems (FMAS 2023), Leiden, The Netherlands, 15-16 November 2023, pp. 77-94. (doi: 10.4204/EPTCS.395.6)

Hunter, Ethan T. P. ORCID logoORCID: https://orcid.org/0000-0002-4309-6861, Enright, Jessica ORCID logoORCID: https://orcid.org/0000-0002-0266-3292 and Miller, Alice A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2023) Feasibility assessments of a dynamical approach to compartmental modelling on graphs: scaling limits and performance analysis. Theoretical Computer Science, 980, 114247. (doi: 10.1016/j.tcs.2023.114247)

2022

Purchase, Helen ORCID logoORCID: https://orcid.org/0000-0001-6994-4446 and Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2022) Mix-and-Match MCQs: Four for the Price of One. In: 27th Annual Conference on Innovation and Technology in Computer Science Education (ITiCSE), Dublin, Ireland, 08-13 July 2022, pp. 593-594. ISBN 9781450392006 (doi: 10.1145/3502717.3532154)

2021

Pagojus, Daumantas, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Porr, Bernd ORCID logoORCID: https://orcid.org/0000-0001-8157-998X and Valkov, Ivaylo ORCID logoORCID: https://orcid.org/0000-0003-1116-875X (2021) Simulation and Model Checking for Close to Real-time Overtaking Planning. In: Third Workshop on Formal Methods for Autonomous Systems (FMAS2021), 21-22 Oct 2021, pp. 20-37. (doi: 10.4204/EPTCS.348.2)

Asogbon, Mojisola Grace, Lu, Yu, Samuel, Oluwarotimi Williams, Jing, Liwen, Miller, Alice A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Li, Guanglin and Wong, Kelvin K.L. (2021) GBRAMP: A generalized backtracking regularized adaptive matching pursuit algorithm for signal reconstruction. Computers and Electrical Engineering, 92, 107189. (doi: 10.1016/j.compeleceng.2021.107189)

Kavanagh, William ORCID logoORCID: https://orcid.org/0000-0003-0521-1643 and Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2021) Gameplay analysis of multiplayer games with verified action-costs. Computer Games Journal, 10(1-4), pp. 89-110. (doi: 10.1007/s40869-020-00121-5)

Kavanagh, William ORCID logoORCID: https://orcid.org/0000-0003-0521-1643, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Norman, Gethin ORCID logoORCID: https://orcid.org/0000-0001-9326-4344 and Andrei, Oana ORCID logoORCID: https://orcid.org/0000-0002-1306-0219 (2021) Balancing turn-based games with chained strategy generation. IEEE Transactions on Games, 13(2), pp. 113-122. (doi: 10.1109/TG.2019.2943227)

Davies, Vinny ORCID logoORCID: https://orcid.org/0000-0003-1896-8936, Wandy, Joe ORCID logoORCID: https://orcid.org/0000-0002-3068-4664, Weidt, Stefan, van der Hooft, Justin J.J. ORCID logoORCID: https://orcid.org/0000-0002-9340-5511, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Daly, Rónán ORCID logoORCID: https://orcid.org/0000-0002-1275-6820 and Rogers, Simon ORCID logoORCID: https://orcid.org/0000-0003-3578-4477 (2021) Rapid development of improved data-dependent acquisition strategies. Analytical Chemistry, 93(14), pp. 5676-5683. (doi: 10.1021/acs.analchem.0c03895) (PMID:33784814) (PMCID:PMC8047769)

Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Barr, Matthew ORCID logoORCID: https://orcid.org/0000-0002-5147-0673, Kavanagh, William ORCID logoORCID: https://orcid.org/0000-0003-0521-1643, Valkov, Ivaylo ORCID logoORCID: https://orcid.org/0000-0003-1116-875X and Purchase, Helen C. ORCID logoORCID: https://orcid.org/0000-0001-6994-4446 (2021) Breakout group allocation schedules and the social golfer problem with adjacent group sizes. Symmetry, 13(1), 13. (doi: 10.3390/sym13010013)

2020

Porr, Bernd ORCID logoORCID: https://orcid.org/0000-0001-8157-998X, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Trew, Alexander (2020) An investigation into serotonergic and environmental interventions against depression in a simulated delayed reward paradigm. Adaptive Behavior, 28(4), pp. 241-260. (doi: 10.1177/1059712319864278)

Fraser, Douglas, Giaquinta, Ruben, Hoffmann, Ruth, Ireland, Murray, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Norman, Gethin ORCID logoORCID: https://orcid.org/0000-0001-9326-4344 (2020) Collaborative models for autonomous systems controller synthesis. Formal Aspects of Computing, 32, pp. 157-186. (doi: 10.1007/s00165-020-00508-1)

Wallis, William, Kavanagh, William, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Storer, Tim ORCID logoORCID: https://orcid.org/0000-0002-4026-097X (2020) Designing a Mobile Game to Generate Player Data - Lessons Learned. In: GAME-ON 2020, Aveiro, Portugal, 23-25 Sept 2020, ISBN 9789492859112

2019

Codish, Michael, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Prosser, Patrick ORCID logoORCID: https://orcid.org/0000-0003-4460-6912 and Stuckey, Peter J. (2019) Constraints for symmetry breaking in graph representation. Constraints, 24(1), pp. 1-24. (doi: 10.1007/s10601-018-9294-5)

Kavanagh, William and Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2019) Chained Strategy Generation: A Technique for Balancing Multiplayer Games Using Model Checking. In: 26th Automated Reasoning Workshop (ARW 2019), London, UK, 02-03 Sep 2019, pp. 15-16.

Valkov, Ivaylo ORCID logoORCID: https://orcid.org/0000-0003-1116-875X and Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2019) Using Model Checking in the Design of a Sensor Network Protocol. In: 26th Automated Reasoning Workshop (ARW 2019), London, UK, 02-03 Sep 2019, pp. 17-18.

2018

Giaquinta, Ruben, Hoffmann, Ruth, Ireland, Murray ORCID logoORCID: https://orcid.org/0000-0001-9091-7071, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Norman, Gethin ORCID logoORCID: https://orcid.org/0000-0001-9326-4344 (2018) Strategy Synthesis for Autonomous Agents Using PRISM. In: 10th NASA Formal Methods Symposium (NFM 2018), Newport News, VA, USA, 17-19 Apr 2018, pp. 220-236. ISBN 9783319779348 (doi: 10.1007/978-3-319-77935-5_16)

2017

Kehrer, Timo and Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (Eds.) (2017) Proceedings Third Workshop on Graphs as Models. EPTCS.

Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Miron, Dragos and Maiya, Sharan (2017) GraphDraw—A Tool for the Represention of Graphs Using Inherent Symmetry. Symmetry 2017: The First International Conference on Symmetry, Barcelona, Spain, 16-18 Oct 2017.

2016

Kirwan, Ryan, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Porr, Bernd ORCID logoORCID: https://orcid.org/0000-0001-8157-998X (2016) Model checking learning agent systems using Promela with embedded C code and abstraction. Formal Aspects of Computing, 28(6), pp. 1027-1056. (doi: 10.1007/s00165-016-0382-2)

Lu, Yu ORCID logoORCID: https://orcid.org/0000-0002-7799-9794, Miller, Alice A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Hoffmann, Ruth and Johnson, Christopher W. ORCID logoORCID: https://orcid.org/0000-0002-1052-9851 (2016) Towards the automated verification of Weibull distributions for system failure rates. Lecture Notes in Computer Science, 9933, pp. 81-96. (doi: 10.1007/978-3-319-45943-1_6)

Peng, Zhaoguang, Lu, Yu ORCID logoORCID: https://orcid.org/0000-0002-7799-9794 and Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2016) Uncertainty Analysis of Phased Mission Systems with Probabilistic Timed Automata. In: 7th IEEE International Conference on Prognostics and Health Management (PHM 2016), Ottawa, Canada, 20-22 June 2016, ISBN 9781509003822 (doi: 10.1109/ICPHM.2016.7542823)

Codish, Michael, Frank, Michael, Itzhakov, Avraham and Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2016) Computing the Ramsey number R(4,3,3) using abstraction and symmetry breaking. Constraints, 21(3), pp. 375-393. (doi: 10.1007/s10601-016-9240-3)

Hoffmann, Ruth, Ireland, Murray ORCID logoORCID: https://orcid.org/0000-0001-9091-7071, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Norman, Gethin ORCID logoORCID: https://orcid.org/0000-0001-9326-4344 and Veres, Sandor (2016) Autonomous agent behaviour modelled in PRISM: a case study. Lecture Notes in Computer Science, 9641, pp. 104-110. (doi: 10.1007/978-3-319-32582-8_7)

Peng, Zhaoguang, Lu, Yu ORCID logoORCID: https://orcid.org/0000-0002-7799-9794, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Tingdi, Zhao and Johnson, Chris ORCID logoORCID: https://orcid.org/0000-0002-1052-9851 (2016) Formal specification and quantitative analysis of a constellation of navigation satellites. Quality and Reliability Engineering International, 32(2), pp. 345-361. (doi: 10.1002/qre.1754)

Peng, Zhaoguang, Lu, Yu ORCID logoORCID: https://orcid.org/0000-0002-7799-9794, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Johnson, Chris ORCID logoORCID: https://orcid.org/0000-0002-1052-9851 and Zhao, Tingdi (2016) Risk assessment of railway transportation systems using timed fault trees. Quality and Reliability Engineering International, 32(1), pp. 181-194. (doi: 10.1002/qre.1738)

2015

Lu, Yu ORCID logoORCID: https://orcid.org/0000-0002-7799-9794, Peng, Zhaoguang, Miller, Alice A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Zhao, Tingdi and Johnson, Christopher W. ORCID logoORCID: https://orcid.org/0000-0002-1052-9851 (2015) How reliable is satellite navigation for aviation? Checking availability properties with probabilistic verification. Reliability Engineering and System Safety, 144, pp. 95-116. (doi: 10.1016/j.ress.2015.07.020)

Macdonald, Craig ORCID logoORCID: https://orcid.org/0000-0003-3143-279X, McCreesh, Ciaran, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Prosser, Patrick ORCID logoORCID: https://orcid.org/0000-0003-4460-6912 (2015) Constructing sailing match race schedules: round-robin pairing lists. In: 21st International Conference on Principles and Practice of Constraint Programming (CP 2015), Cork, Ireland, 31 Aug -04 Sep 2015, pp. 671-686. ISBN 9783319232188 (doi: 10.1007/978-3-319-23219-5_46)

Codish, Michael, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Frank, Michael and Itzhakov, Avraham (2015) Solving graph coloring problems with abstraction and symmetry. In: Fifth International Workshop on the Cross-Fertilization Between CSP and SAT, Cork, Ireland, 31 Aug 2015,

Lu, Yu ORCID logoORCID: https://orcid.org/0000-0002-7799-9794, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Johnson, Christopher ORCID logoORCID: https://orcid.org/0000-0002-1052-9851, Peng, Zhaoguang and Zhao, Tingdi (2015) Availability analysis of satellite positioning systems for aviation using the prism model checker. In: 17th IEEE International Conference on Computational Science and Engineering (CSE 2014), Chengdu, China, 19-21 Dec 2014, pp. 704-713. (doi: 10.1109/CSE.2014.148)

2014

Lu, Yu ORCID logoORCID: https://orcid.org/0000-0002-7799-9794, Peng, Zhaoguang, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Zhao, Tingdi and Johnson, Chris ORCID logoORCID: https://orcid.org/0000-0002-1052-9851 (2014) Timed Fault Tree Models of the China Yongwen Railway Accident. In: 8th Asia Modelling Symposium (AMS 2014), Taipei, Taiwan, 23-25 Sep 2014, pp. 128-133. ISBN 9781479964864 (doi: 10.1109/AMS.2014.34)

Gibson, Emma K. ORCID logoORCID: https://orcid.org/0000-0002-7839-3786, Winfield, John M., Adam, David, Miller, Alice A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Carr, Robert H., Eaglesham, Archie and Lennon, David ORCID logoORCID: https://orcid.org/0000-0001-8397-0528 (2014) The solvation and dissociation of 4-benzylaniline hydrochloride in chlorobenzene. Industrial and Engineering Chemistry Research, 53(11), pp. 4156-4164. (doi: 10.1021/ie403745s)

2013

Kirwan, Ryan, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Porr, Bernd ORCID logoORCID: https://orcid.org/0000-0001-8157-998X and Di Prodi, P. (2013) Formal modeling of robot behavior with learning. Neural Computation, 25(11), pp. 2976-3019. (doi: 10.1162/NECO_a_00493)

Codish, M., Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Prosser, P. ORCID logoORCID: https://orcid.org/0000-0003-4460-6912 and Stuckey, A. (2013) Breaking Symmetries in Graph Representation. In: International Joint Conference on Artificial Intelligence, Beijing, China, 3-9 Aug 2013,

Kirwan, R. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2013) Formal proof of abstraction for agent-based learning systems. In: 20th Workshop on Automated Reasoning ARW 2013, Dundee, UK, 11-12 Apr 2013,

Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Kirwan, R., Porr, B. ORCID logoORCID: https://orcid.org/0000-0001-8157-998X and Di Prodi, P. (2013) Model checking for improved adaptive behaviour. In: Proceedings of the Institution of Engineering and Technology Conference on Control and Automation, Birmingham, England, 4-5 Jun 2013,

Peng, Z., Lu, Y. ORCID logoORCID: https://orcid.org/0000-0002-7799-9794, Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Johnson, C. ORCID logoORCID: https://orcid.org/0000-0002-1052-9851 and Zhao, T. (2013) A probabilistic model checking approach to analysing reliability, availability, and maintainability of a single satellite system. In: 7th European Modelling Symposium (EMS2013), Manchester, England, 20-22 Nov 2013, pp. 611-616. (doi: 10.1109/EMS.2013.102)

2012

Lu, Y. ORCID logoORCID: https://orcid.org/0000-0002-7799-9794 and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2012) Timed analysis of RFID distance bounding protocols. In: Schmidt, R.A. and Papacchini, F. (eds.) Proceedings of the 19th Workshop on Automated Reasoning ARW 2012, Manchester, UK, 2-4 Apr 2012. School of Computer Science, The University of Manchester: Manchester, pp. 37-38.

Andrei, O. ORCID logoORCID: https://orcid.org/0000-0002-1306-0219, Calder, M. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2012) Role-Based Interface Automata. In: 4th International Workshop on Foundations of Interface Technologies, Tallinn, Estonia, 25 Mar 2012,

Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232, Gray, P., Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Unsworth, C. (2012) An Introduction to Pervasive Interface Automata. Lecture Notes in Computer Science, 6921, pp. 71-87. (doi: 10.1007/978-3-642-27269-1_5)

Kirwan, R. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2012) Progress on model checking robot behaviour. In: Schmidt, R.A. and Papacchini, F. (eds.) Proceedings of the 19th Workshop on Automated Reasoning ARW 2012, Manchester, UK, 2-4 Apr 2012. School of Computer Science, The University of Manchester: Manchester, pp. 39-40.

Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Prosser, P. ORCID logoORCID: https://orcid.org/0000-0003-4460-6912 (2012) Diamond-free degree sequences. Acta Universitatis Sapientiae, Informatica, 4(2), pp. 189-200.

Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2012) A Collection of Linear Spaces of Order 16 with Block Size 4, with Diamond-Free Complement Graphs. Technical Report. School of Computing Science, University of Glasgow.

2011

Kirwan, R. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2011) Abstraction for model checking robot behaviour. In: Kirwan, R. and Miller, A. (eds.) Proceedings of the 18th Workshop on Automated Reasoning ARW 2011, Glasgow, UK, 11-12 Apr 2011. Department of Computing Science, University of Glasgow: Glasgow, UK, pp. 1-2.

2010

Kirwan, R. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2010) Modelling multi-agent systems. In: Automated Reasoning Workshop 2010 Bridging the Gap between Theory and Practice ARW 2010, Harrow, UK, 30-31 Mar 2010, pp. 18-19.

Power, C. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2010) An approach to probabilistic symmetry reduction. In: Automated Reasoning Workshop 2010 Bridging the Gap between Theory and Practice ARW 2010, Harrow, UK, 30-31 Mar 2010, pp. 32-33.

Ripon, S. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2010) Verification of a symmetry detection technique using PVS. In: 10th International Workshop on Automated Verification of Critical Systems (AVoCS'2010), Düsseldorf, Germany, September 21-23, 2010,

2009

Arapinis, M. et al. (2009) Towards the verification of pervasive systems. Electronic Communications of the EASST, 22,

Donaldson, A. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2009) On the constructive orbit problem. Annals of Mathematics and Artificial Intelligence, 57(1), pp. 1-35. (doi: 10.1007/s10472-009-9171-4)

Donaldson, A.F., Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Parker, D. (2009) Language-level symmetry reduction for probabilistic model checking. In: 6th International Conference on the Quantitative Evaluation of Systems, Budapest, 13-16 Sept 2009, pp. 289-298. (doi: 10.1109/QEST.2009.21)

Graham, D., Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2009) An inductive technique for parameterised model checking of degenerative distributed randomised protocols. Electronic Notes in Theoretical Computer Science, 250(1), pp. 87-103. (doi: 10.1016/j.entcs.2009.08.007)

Miller, A ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Calder, M ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 (2009) Preface to Proceedings of the Eighth International Workshop on Automated Verification of Critical Systems. Electronic Notes in Theoretical Computer Science, 250(2), pp. 1-2. (doi: 10.1016/j.entcs.2009.08.013)

Power, C. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2009) Symmetry reduction of partially symmetric systems. In: Hustadt, U. (ed.) Proceedings of the Automated Reasoning Workshop 2009: Bridging the Gap between Theory and Practice ARW 2009, Liverpool, UK, 21-22 Sep 2009. University of Liverpool: Liverpool, UK, pp. 25-26.

Ripon, S., Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Donaldson, S. (2009) A semantic embedding of Prolema-Lite in PVS. In: Ninth International Workshop on Automated Verification of Critical Systems (AVOCS 09), Swansea, Wales, 23-25 Sep 2009,

Sharma, O., Lewis, J., Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Dearle, A., Balasubramaniam, D., Morrison, R. and Sventek, J. (2009) Towards verifying correctness of wireless sensor network applications using insense and spin. Lecture Notes in Computer Science, 5578, pp. 223-240. (doi: 10.1007/978-3-642-02652-2_19)

2008

Donaldson, A.F. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2008) Automatic symmetry detection for Promela. Journal of Automated Reasoning, 41(3-4), pp. 251-293. (doi: 10.1007/s10817-008-9107-4)

Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2008) An automatic abstraction technique for verifying featured, parameterised systems. Theoretical Computer Science, 404(3), pp. 235-255. (doi: 10.1016/j.tcs.2008.03.034)

Power, C. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2008) Prism2Promela. In: Fifth International Conference on Quantitative Evaluation of Systems, 2008. QEST '08, St. Malo, France, 14-17 Sep 2008, pp. 79-80. ISBN 978-0-7695-3360-5 (doi: 10.1109/QEST.2008.20)

2007

Miller, A., Calder, M. and Donaldson, A.F. (2007) A template-based approach for the generation of abstractable and reducible models of featured networks. Computer Networks, 51(2), pp. 439-455. (doi: 10.1016/j.comnet.2006.08.009)

Donaldson, A. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2007) Symmetry reduction techniques for explicit-state model checking. In: First International Symmetry Conference, Edinburgh, UK, 14-17 Jan 07, pp. 41-45.

Donaldson, A.F. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2007) Extending symmetry reduction techniques to a realistic model of computation. In: 6th International Workshop on Automated Verification of Critical Systems AVoCS, Nancy, France, 18-19 Sep 2006,

Donaldson, A.F., Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Parker, D. (2007) GRIP: generic representatives in PRISM. In: Proceedings of the Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007), Edinburgh, UK, 17-19 Sep 2007. IEEE Computer Society: Los Alamitos, CA, USA, pp. 115-116. ISBN 9780769528830 (doi: 10.1109/QEST.2007.30)

Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Donaldson, A.F. (2007) Symmetry reduction methods for model checking. In: Automated Reasoning Workshop 2007, London, UK, 19-20 Apr 2007,

2006

Ballarini, P. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2006) Model checking medium access control for sensor networks. In: Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation ISoLA 2006, Paphos, Cyprus, 15-19 November 2006, pp. 255-262. (doi: 10.1109/ISoLA.2006.16)

Donaldson, A.F. and Miller, A. (2006) A computational group theoretic symmetry reduction package for the SPIN model checker. Lecture Notes in Computer Science, 4019, pp. 374-380. (doi: 10.1007/11784180)

Miller, A., Donaldson, A. and Calder, M. (2006) Symmetry in temporal logic model checking. ACM Computing Surveys, 38(3), (doi: 10.1145/1132960.1132962)

Donaldson, A.F and Miller, A. (2006) Exact and approximate strategies for symmetry reduction in model checking. Lecture Notes in Computer Science, 4085, pp. 541-556. (doi: 10.1007/11813040)

Calder, M. and Miller, A. (2006) Feature interaction detection by pairwise analysis of LTL properties—A case study. Formal Methods in System Design, 28(3), pp. 213-261. (doi: 10.1007/s10703-006-0002-5)

Donaldson, A.F. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2006) Evaluating a formal methods technique via student assessed exercises. In: Boute, R.T. and Oliveira, J.N. (eds.) Formal Methods in the Teaching Lab: Examples, Cases, Assignments and Projects Enhancing Formal Methods Education. A Workshop at the Formal Methods 2006 Symposium, Hamilton, Ontario, Canada, 26 Aug 2006. McMaster University: Hamilton, ON, Canada, pp. 93-98.

Donaldson, AF and Miller, A ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2006) Symmetry reduction for probabilistic model checking using generic representatives. Automated Technology For Verification and Analysis, Proceedings, 4218, pp. 9-23.

Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Cutts, Q. ORCID logoORCID: https://orcid.org/0000-0002-6368-9912 (2006) The use of an electronic voting system in a formal methods course. In: Boute, R.T. and Oliveira, J.N. (eds.) Formal Methods in the Teaching Lab: Examples, Cases, Assignments and Projects Enhancing Formal Methods Education. A Workshop at the Formal Methods 2006 Symposium, Hamilton, Ontario, Canada, 26 Aug 2006. McMaster University: Hamilton, ON, Canada, pp. 3-8.

2005

Donaldson, A., Miller, A and Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 (2005) SPIN-to-GRAPE: a tool for analysing symmetry in Promela models. Electronic Notes in Theoretical Computer Science, 139(1), pp. 3-23. (doi: 10.1016/j.entcs.2005.09.007)

Donaldson, A.F., Miller, A. and Calder, M. (2005) Finding symmetry in models of concurrent systems by static channel diagram analysis. Theoretical Computer Science, 128(6), pp. 161-177. (doi: 10.1016/j.entcs.2005.04.010)

Donaldson, A.F. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2005) Symmetry reduction for probabilistic systems. In: The 12th Workshop on Automated Reasoning: Bridging the Gap Between Theory and Practice, Edinburgh, UK, 29-30 Jul 2005, pp. 17-18.

Donaldson, A.F. and Miller, A. (2005) Automatic symmetry detection for model checking using computational group theory. Lecture Notes in Computer Science, 3582, pp. 481-496. (doi: 10.1007/11526841_32)

Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2005) Improved lower bounds for solving the minimal open stacks problem. In: Constraint Modelling Challenge 2005, in Conjunction with The Fifth Workshop on Modelling and Solving Problems with Constraints Held at IJCAI 2005, Edinburgh, Scotland, 31 Jul 2005. School of Computer Science, University of St. Andrews: St. Andrews, UK, pp. 36-43.

Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Prosser, P. ORCID logoORCID: https://orcid.org/0000-0003-4460-6912 and Unsworth, C. (2005) A constraint model and a reduction operator for the minimising open stacks problem. In: Constraint Modelling Challenge 2005, in Conjunction with The Fifth Workshop on Modelling and Solving Problems with Constraints Held at IJCAI 2005, Edinburgh, Scotland, 31 Jul 2005. School of Computer Science, University of St. Andrews: St. Andrews, UK, pp. 44-50.

Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 (2005) A generic approach for the automatic verification of featured, parameterised systems. In: International Workshop on Feature Interactions in Telecommunications and Software Systems, Leicester, UK, 28-30 June 2005, pp. 217-235. ISBN 158603524X

2004

Calder, M. and Miller, A. (2004) An automatic abstraction technique for verifying featured, parameterised systems. In: ISOLA: International Symposium on Leveraging Applications of Formal Methods, Cyprus, Greece, 30 Oct - 2 Nov 2004, pp. 227-234.

Calder, M. and Miller, A. (2004) Detecting feature interactions: how many components do we need? Lecture Notes in Computer Science, 2975, pp. 45-66. (doi: 10.1007/b97772)

Donaldson, A., Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 (2004) Comparing the use of symmetry in constraint processing and model checking. In: 4th International Workshop on Symmetry and Constraint Satisfaction Problems, Toronto, Ontario, Canada, 27 Sep 2004, pp. 18-25.

Gregory, P., Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Prosser, P. ORCID logoORCID: https://orcid.org/0000-0003-4460-6912 (2004) Solving the rehearsal problem with planning and with model checking. In: Workshop on Modelling and Solving Problems with Constraints, Valencia, Spain, 22 Aug 2004, pp. 157-171.

2003

Calder, M. and Miller, A. (2003) Generalising feature interactions in email. In: International Workshop on Feature Interactions in Telecommunications and Software Systems VII, Ottawa, Canada, 11-13 June 2003, pp. 187-205. ISBN 1586033484

Calder, M. and Miller, A. (2003) Using SPIN to Analyse the Tree Identification Phase of the IEEE 1394 High-Performance Serial Bus(FireWire)Protocol. Formal Aspects of Computing, 14(3), pp. 247-266. (doi: 10.1007/s001650300004)

Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 (2003) An application of abstraction and induction techniques to degenerating systems of processes. In: International Workshop on Model-Checking for Dependable Software-Intensive Systems, San Francisco, CA, USA, 22-25 Jun 2003, W75-W79.

2002

Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2002) Five ways to use induction and symmetry in the verification of networks of processes by model-checking. In: Second Workshop on Automated Verification of Critical Systems (AVoCS 2002), April 2002, pp. 29-42.

Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2002) Automatic verification of any number of concurrent, communicating processes. In: 17th IEEE International Conference on Automated Software Engineering, Edinburgh, 23-27 September, pp. 227-230. ISBN 0769517366 (doi: 10.1109/ASE.2002.1115017)

2001

Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2001) Using SPIN for feature interaction analysis - a case study. Lecture Notes in Computer Science, 2057, pp. 143-162.

Miller, A ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2001) Using SPIN for Feature Interaction Analysis -- a Case Study. Proceedings of the 8th International Spin Workshop (spin 2001), pp. 143-162.

1998

Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (1998) Analysing a basic call protocol using Promela/XSpin. In: 4th Workshop on Automata Theoretic Verification with the SPIN Model Checker (SPIN '98), Paris, France, 2 Nov 1998, pp. 1-12.

1996

Camina, A.R. and Miller, A.A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (1996) Line-closed subsets of Steiner triple systems and classical linear spaces. Journal of Statistical Planning and Inference, 56(1), pp. 65-77. (doi: 10.1016/S0378-3758(96)00010-9)

1994

Miller, A.A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Praeger, C.E. (1994) Non-Cayley vertex-transitive graphs of order twice the product of two odd primes. Journal of Algebraic Combinatorics, 3(1), pp. 77-111. (doi: 10.1023/A:1022402204659)

1991

Miller, A.A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (1991) A subspace theorem for ordinary linear differential equations. Journal of the Australian Mathematical Society, 50(2), pp. 320-332. (doi: 10.1017/S144678870003278X)

This list was generated on Sat Jun 14 10:15:00 2025 BST.
Jump to: Articles | Book Sections | Edited Books | Research Reports or Papers | Conference or Workshop Item | Conference Proceedings
Number of items: 96.

Articles

Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Porr, Bernd ORCID logoORCID: https://orcid.org/0000-0001-8157-998X, Valkov, Ivaylo ORCID logoORCID: https://orcid.org/0000-0003-1116-875X, Fraser, Douglas and Pagojus, Daumantas (2025) Model checking with memoisation for fast overtaking planning. Science of Computer Programming, 244, 103300. (doi: 10.1016/j.scico.2025.103300)

Lafratta, Giulia ORCID logoORCID: https://orcid.org/0009-0006-2072-338X, Porr, Bernd ORCID logoORCID: https://orcid.org/0000-0001-8157-998X, Chandler, Christopher ORCID logoORCID: https://orcid.org/0000-0001-5025-1498 and Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2025) Closed-loop multi-step planning. Neural Computation, (Accepted for Publication)

Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Abel, Julian R., Valkov, Ivaylo ORCID logoORCID: https://orcid.org/0000-0003-1116-875X and Fraser, Douglas (2024) Implementing the MOLS table for n up to 500. Symmetry, 16(12), 1678. (doi: 10.3390/sym16121678)

Hunter, Ethan T. P. ORCID logoORCID: https://orcid.org/0000-0002-4309-6861, Enright, Jessica ORCID logoORCID: https://orcid.org/0000-0002-0266-3292 and Miller, Alice A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2023) Feasibility assessments of a dynamical approach to compartmental modelling on graphs: scaling limits and performance analysis. Theoretical Computer Science, 980, 114247. (doi: 10.1016/j.tcs.2023.114247)

Asogbon, Mojisola Grace, Lu, Yu, Samuel, Oluwarotimi Williams, Jing, Liwen, Miller, Alice A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Li, Guanglin and Wong, Kelvin K.L. (2021) GBRAMP: A generalized backtracking regularized adaptive matching pursuit algorithm for signal reconstruction. Computers and Electrical Engineering, 92, 107189. (doi: 10.1016/j.compeleceng.2021.107189)

Kavanagh, William ORCID logoORCID: https://orcid.org/0000-0003-0521-1643 and Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2021) Gameplay analysis of multiplayer games with verified action-costs. Computer Games Journal, 10(1-4), pp. 89-110. (doi: 10.1007/s40869-020-00121-5)

Kavanagh, William ORCID logoORCID: https://orcid.org/0000-0003-0521-1643, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Norman, Gethin ORCID logoORCID: https://orcid.org/0000-0001-9326-4344 and Andrei, Oana ORCID logoORCID: https://orcid.org/0000-0002-1306-0219 (2021) Balancing turn-based games with chained strategy generation. IEEE Transactions on Games, 13(2), pp. 113-122. (doi: 10.1109/TG.2019.2943227)

Davies, Vinny ORCID logoORCID: https://orcid.org/0000-0003-1896-8936, Wandy, Joe ORCID logoORCID: https://orcid.org/0000-0002-3068-4664, Weidt, Stefan, van der Hooft, Justin J.J. ORCID logoORCID: https://orcid.org/0000-0002-9340-5511, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Daly, Rónán ORCID logoORCID: https://orcid.org/0000-0002-1275-6820 and Rogers, Simon ORCID logoORCID: https://orcid.org/0000-0003-3578-4477 (2021) Rapid development of improved data-dependent acquisition strategies. Analytical Chemistry, 93(14), pp. 5676-5683. (doi: 10.1021/acs.analchem.0c03895) (PMID:33784814) (PMCID:PMC8047769)

Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Barr, Matthew ORCID logoORCID: https://orcid.org/0000-0002-5147-0673, Kavanagh, William ORCID logoORCID: https://orcid.org/0000-0003-0521-1643, Valkov, Ivaylo ORCID logoORCID: https://orcid.org/0000-0003-1116-875X and Purchase, Helen C. ORCID logoORCID: https://orcid.org/0000-0001-6994-4446 (2021) Breakout group allocation schedules and the social golfer problem with adjacent group sizes. Symmetry, 13(1), 13. (doi: 10.3390/sym13010013)

Porr, Bernd ORCID logoORCID: https://orcid.org/0000-0001-8157-998X, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Trew, Alexander (2020) An investigation into serotonergic and environmental interventions against depression in a simulated delayed reward paradigm. Adaptive Behavior, 28(4), pp. 241-260. (doi: 10.1177/1059712319864278)

Fraser, Douglas, Giaquinta, Ruben, Hoffmann, Ruth, Ireland, Murray, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Norman, Gethin ORCID logoORCID: https://orcid.org/0000-0001-9326-4344 (2020) Collaborative models for autonomous systems controller synthesis. Formal Aspects of Computing, 32, pp. 157-186. (doi: 10.1007/s00165-020-00508-1)

Codish, Michael, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Prosser, Patrick ORCID logoORCID: https://orcid.org/0000-0003-4460-6912 and Stuckey, Peter J. (2019) Constraints for symmetry breaking in graph representation. Constraints, 24(1), pp. 1-24. (doi: 10.1007/s10601-018-9294-5)

Kirwan, Ryan, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Porr, Bernd ORCID logoORCID: https://orcid.org/0000-0001-8157-998X (2016) Model checking learning agent systems using Promela with embedded C code and abstraction. Formal Aspects of Computing, 28(6), pp. 1027-1056. (doi: 10.1007/s00165-016-0382-2)

Lu, Yu ORCID logoORCID: https://orcid.org/0000-0002-7799-9794, Miller, Alice A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Hoffmann, Ruth and Johnson, Christopher W. ORCID logoORCID: https://orcid.org/0000-0002-1052-9851 (2016) Towards the automated verification of Weibull distributions for system failure rates. Lecture Notes in Computer Science, 9933, pp. 81-96. (doi: 10.1007/978-3-319-45943-1_6)

Codish, Michael, Frank, Michael, Itzhakov, Avraham and Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2016) Computing the Ramsey number R(4,3,3) using abstraction and symmetry breaking. Constraints, 21(3), pp. 375-393. (doi: 10.1007/s10601-016-9240-3)

Hoffmann, Ruth, Ireland, Murray ORCID logoORCID: https://orcid.org/0000-0001-9091-7071, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Norman, Gethin ORCID logoORCID: https://orcid.org/0000-0001-9326-4344 and Veres, Sandor (2016) Autonomous agent behaviour modelled in PRISM: a case study. Lecture Notes in Computer Science, 9641, pp. 104-110. (doi: 10.1007/978-3-319-32582-8_7)

Peng, Zhaoguang, Lu, Yu ORCID logoORCID: https://orcid.org/0000-0002-7799-9794, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Tingdi, Zhao and Johnson, Chris ORCID logoORCID: https://orcid.org/0000-0002-1052-9851 (2016) Formal specification and quantitative analysis of a constellation of navigation satellites. Quality and Reliability Engineering International, 32(2), pp. 345-361. (doi: 10.1002/qre.1754)

Peng, Zhaoguang, Lu, Yu ORCID logoORCID: https://orcid.org/0000-0002-7799-9794, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Johnson, Chris ORCID logoORCID: https://orcid.org/0000-0002-1052-9851 and Zhao, Tingdi (2016) Risk assessment of railway transportation systems using timed fault trees. Quality and Reliability Engineering International, 32(1), pp. 181-194. (doi: 10.1002/qre.1738)

Lu, Yu ORCID logoORCID: https://orcid.org/0000-0002-7799-9794, Peng, Zhaoguang, Miller, Alice A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Zhao, Tingdi and Johnson, Christopher W. ORCID logoORCID: https://orcid.org/0000-0002-1052-9851 (2015) How reliable is satellite navigation for aviation? Checking availability properties with probabilistic verification. Reliability Engineering and System Safety, 144, pp. 95-116. (doi: 10.1016/j.ress.2015.07.020)

Gibson, Emma K. ORCID logoORCID: https://orcid.org/0000-0002-7839-3786, Winfield, John M., Adam, David, Miller, Alice A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Carr, Robert H., Eaglesham, Archie and Lennon, David ORCID logoORCID: https://orcid.org/0000-0001-8397-0528 (2014) The solvation and dissociation of 4-benzylaniline hydrochloride in chlorobenzene. Industrial and Engineering Chemistry Research, 53(11), pp. 4156-4164. (doi: 10.1021/ie403745s)

Kirwan, Ryan, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Porr, Bernd ORCID logoORCID: https://orcid.org/0000-0001-8157-998X and Di Prodi, P. (2013) Formal modeling of robot behavior with learning. Neural Computation, 25(11), pp. 2976-3019. (doi: 10.1162/NECO_a_00493)

Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232, Gray, P., Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Unsworth, C. (2012) An Introduction to Pervasive Interface Automata. Lecture Notes in Computer Science, 6921, pp. 71-87. (doi: 10.1007/978-3-642-27269-1_5)

Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Prosser, P. ORCID logoORCID: https://orcid.org/0000-0003-4460-6912 (2012) Diamond-free degree sequences. Acta Universitatis Sapientiae, Informatica, 4(2), pp. 189-200.

Arapinis, M. et al. (2009) Towards the verification of pervasive systems. Electronic Communications of the EASST, 22,

Donaldson, A. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2009) On the constructive orbit problem. Annals of Mathematics and Artificial Intelligence, 57(1), pp. 1-35. (doi: 10.1007/s10472-009-9171-4)

Graham, D., Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2009) An inductive technique for parameterised model checking of degenerative distributed randomised protocols. Electronic Notes in Theoretical Computer Science, 250(1), pp. 87-103. (doi: 10.1016/j.entcs.2009.08.007)

Miller, A ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Calder, M ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 (2009) Preface to Proceedings of the Eighth International Workshop on Automated Verification of Critical Systems. Electronic Notes in Theoretical Computer Science, 250(2), pp. 1-2. (doi: 10.1016/j.entcs.2009.08.013)

Sharma, O., Lewis, J., Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Dearle, A., Balasubramaniam, D., Morrison, R. and Sventek, J. (2009) Towards verifying correctness of wireless sensor network applications using insense and spin. Lecture Notes in Computer Science, 5578, pp. 223-240. (doi: 10.1007/978-3-642-02652-2_19)

Donaldson, A.F. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2008) Automatic symmetry detection for Promela. Journal of Automated Reasoning, 41(3-4), pp. 251-293. (doi: 10.1007/s10817-008-9107-4)

Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2008) An automatic abstraction technique for verifying featured, parameterised systems. Theoretical Computer Science, 404(3), pp. 235-255. (doi: 10.1016/j.tcs.2008.03.034)

Miller, A., Calder, M. and Donaldson, A.F. (2007) A template-based approach for the generation of abstractable and reducible models of featured networks. Computer Networks, 51(2), pp. 439-455. (doi: 10.1016/j.comnet.2006.08.009)

Donaldson, A.F. and Miller, A. (2006) A computational group theoretic symmetry reduction package for the SPIN model checker. Lecture Notes in Computer Science, 4019, pp. 374-380. (doi: 10.1007/11784180)

Miller, A., Donaldson, A. and Calder, M. (2006) Symmetry in temporal logic model checking. ACM Computing Surveys, 38(3), (doi: 10.1145/1132960.1132962)

Donaldson, A.F and Miller, A. (2006) Exact and approximate strategies for symmetry reduction in model checking. Lecture Notes in Computer Science, 4085, pp. 541-556. (doi: 10.1007/11813040)

Calder, M. and Miller, A. (2006) Feature interaction detection by pairwise analysis of LTL properties—A case study. Formal Methods in System Design, 28(3), pp. 213-261. (doi: 10.1007/s10703-006-0002-5)

Donaldson, AF and Miller, A ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2006) Symmetry reduction for probabilistic model checking using generic representatives. Automated Technology For Verification and Analysis, Proceedings, 4218, pp. 9-23.

Donaldson, A., Miller, A and Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 (2005) SPIN-to-GRAPE: a tool for analysing symmetry in Promela models. Electronic Notes in Theoretical Computer Science, 139(1), pp. 3-23. (doi: 10.1016/j.entcs.2005.09.007)

Donaldson, A.F., Miller, A. and Calder, M. (2005) Finding symmetry in models of concurrent systems by static channel diagram analysis. Theoretical Computer Science, 128(6), pp. 161-177. (doi: 10.1016/j.entcs.2005.04.010)

Donaldson, A.F. and Miller, A. (2005) Automatic symmetry detection for model checking using computational group theory. Lecture Notes in Computer Science, 3582, pp. 481-496. (doi: 10.1007/11526841_32)

Calder, M. and Miller, A. (2004) Detecting feature interactions: how many components do we need? Lecture Notes in Computer Science, 2975, pp. 45-66. (doi: 10.1007/b97772)

Calder, M. and Miller, A. (2003) Using SPIN to Analyse the Tree Identification Phase of the IEEE 1394 High-Performance Serial Bus(FireWire)Protocol. Formal Aspects of Computing, 14(3), pp. 247-266. (doi: 10.1007/s001650300004)

Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2001) Using SPIN for feature interaction analysis - a case study. Lecture Notes in Computer Science, 2057, pp. 143-162.

Miller, A ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2001) Using SPIN for Feature Interaction Analysis -- a Case Study. Proceedings of the 8th International Spin Workshop (spin 2001), pp. 143-162.

Camina, A.R. and Miller, A.A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (1996) Line-closed subsets of Steiner triple systems and classical linear spaces. Journal of Statistical Planning and Inference, 56(1), pp. 65-77. (doi: 10.1016/S0378-3758(96)00010-9)

Miller, A.A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Praeger, C.E. (1994) Non-Cayley vertex-transitive graphs of order twice the product of two odd primes. Journal of Algebraic Combinatorics, 3(1), pp. 77-111. (doi: 10.1023/A:1022402204659)

Miller, A.A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (1991) A subspace theorem for ordinary linear differential equations. Journal of the Australian Mathematical Society, 50(2), pp. 320-332. (doi: 10.1017/S144678870003278X)

Book Sections

Lu, Y. ORCID logoORCID: https://orcid.org/0000-0002-7799-9794 and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2012) Timed analysis of RFID distance bounding protocols. In: Schmidt, R.A. and Papacchini, F. (eds.) Proceedings of the 19th Workshop on Automated Reasoning ARW 2012, Manchester, UK, 2-4 Apr 2012. School of Computer Science, The University of Manchester: Manchester, pp. 37-38.

Kirwan, R. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2012) Progress on model checking robot behaviour. In: Schmidt, R.A. and Papacchini, F. (eds.) Proceedings of the 19th Workshop on Automated Reasoning ARW 2012, Manchester, UK, 2-4 Apr 2012. School of Computer Science, The University of Manchester: Manchester, pp. 39-40.

Kirwan, R. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2011) Abstraction for model checking robot behaviour. In: Kirwan, R. and Miller, A. (eds.) Proceedings of the 18th Workshop on Automated Reasoning ARW 2011, Glasgow, UK, 11-12 Apr 2011. Department of Computing Science, University of Glasgow: Glasgow, UK, pp. 1-2.

Power, C. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2009) Symmetry reduction of partially symmetric systems. In: Hustadt, U. (ed.) Proceedings of the Automated Reasoning Workshop 2009: Bridging the Gap between Theory and Practice ARW 2009, Liverpool, UK, 21-22 Sep 2009. University of Liverpool: Liverpool, UK, pp. 25-26.

Donaldson, A.F., Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Parker, D. (2007) GRIP: generic representatives in PRISM. In: Proceedings of the Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007), Edinburgh, UK, 17-19 Sep 2007. IEEE Computer Society: Los Alamitos, CA, USA, pp. 115-116. ISBN 9780769528830 (doi: 10.1109/QEST.2007.30)

Donaldson, A.F. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2006) Evaluating a formal methods technique via student assessed exercises. In: Boute, R.T. and Oliveira, J.N. (eds.) Formal Methods in the Teaching Lab: Examples, Cases, Assignments and Projects Enhancing Formal Methods Education. A Workshop at the Formal Methods 2006 Symposium, Hamilton, Ontario, Canada, 26 Aug 2006. McMaster University: Hamilton, ON, Canada, pp. 93-98.

Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Cutts, Q. ORCID logoORCID: https://orcid.org/0000-0002-6368-9912 (2006) The use of an electronic voting system in a formal methods course. In: Boute, R.T. and Oliveira, J.N. (eds.) Formal Methods in the Teaching Lab: Examples, Cases, Assignments and Projects Enhancing Formal Methods Education. A Workshop at the Formal Methods 2006 Symposium, Hamilton, Ontario, Canada, 26 Aug 2006. McMaster University: Hamilton, ON, Canada, pp. 3-8.

Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2005) Improved lower bounds for solving the minimal open stacks problem. In: Constraint Modelling Challenge 2005, in Conjunction with The Fifth Workshop on Modelling and Solving Problems with Constraints Held at IJCAI 2005, Edinburgh, Scotland, 31 Jul 2005. School of Computer Science, University of St. Andrews: St. Andrews, UK, pp. 36-43.

Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Prosser, P. ORCID logoORCID: https://orcid.org/0000-0003-4460-6912 and Unsworth, C. (2005) A constraint model and a reduction operator for the minimising open stacks problem. In: Constraint Modelling Challenge 2005, in Conjunction with The Fifth Workshop on Modelling and Solving Problems with Constraints Held at IJCAI 2005, Edinburgh, Scotland, 31 Jul 2005. School of Computer Science, University of St. Andrews: St. Andrews, UK, pp. 44-50.

Edited Books

Kehrer, Timo and Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (Eds.) (2017) Proceedings Third Workshop on Graphs as Models. EPTCS.

Research Reports or Papers

Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2012) A Collection of Linear Spaces of Order 16 with Block Size 4, with Diamond-Free Complement Graphs. Technical Report. School of Computing Science, University of Glasgow.

Conference or Workshop Item

Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Miron, Dragos and Maiya, Sharan (2017) GraphDraw—A Tool for the Represention of Graphs Using Inherent Symmetry. Symmetry 2017: The First International Conference on Symmetry, Barcelona, Spain, 16-18 Oct 2017.

Conference Proceedings

Valkov, Ivaylo ORCID logoORCID: https://orcid.org/0000-0003-1116-875X, Donaldson, Alastair and Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2024) Synchronisation in Language-Level Symmetry Reduction for Probabilistic Model Checking. In: 30th International SPIN symposium on Model Checking of Software (SPIN 2024), Luxembourg, 10-11 Apr 2024, pp. 49-66. ISBN 9783031661488 (doi: 10.1007/978-3-031-66149-5_3)

Chandler, Christopher ORCID logoORCID: https://orcid.org/0000-0001-5025-1498, Porr, Bernd ORCID logoORCID: https://orcid.org/0000-0001-8157-998X, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Lafratta, Giulia ORCID logoORCID: https://orcid.org/0009-0006-2072-338X (2023) Model Checking for Closed-Loop Robot Reactive Planning. In: Fifth Workshop on Formal Methods for Autonomous Systems (FMAS 2023), Leiden, The Netherlands, 15-16 November 2023, pp. 77-94. (doi: 10.4204/EPTCS.395.6)

Purchase, Helen ORCID logoORCID: https://orcid.org/0000-0001-6994-4446 and Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2022) Mix-and-Match MCQs: Four for the Price of One. In: 27th Annual Conference on Innovation and Technology in Computer Science Education (ITiCSE), Dublin, Ireland, 08-13 July 2022, pp. 593-594. ISBN 9781450392006 (doi: 10.1145/3502717.3532154)

Pagojus, Daumantas, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Porr, Bernd ORCID logoORCID: https://orcid.org/0000-0001-8157-998X and Valkov, Ivaylo ORCID logoORCID: https://orcid.org/0000-0003-1116-875X (2021) Simulation and Model Checking for Close to Real-time Overtaking Planning. In: Third Workshop on Formal Methods for Autonomous Systems (FMAS2021), 21-22 Oct 2021, pp. 20-37. (doi: 10.4204/EPTCS.348.2)

Wallis, William, Kavanagh, William, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Storer, Tim ORCID logoORCID: https://orcid.org/0000-0002-4026-097X (2020) Designing a Mobile Game to Generate Player Data - Lessons Learned. In: GAME-ON 2020, Aveiro, Portugal, 23-25 Sept 2020, ISBN 9789492859112

Kavanagh, William and Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2019) Chained Strategy Generation: A Technique for Balancing Multiplayer Games Using Model Checking. In: 26th Automated Reasoning Workshop (ARW 2019), London, UK, 02-03 Sep 2019, pp. 15-16.

Valkov, Ivaylo ORCID logoORCID: https://orcid.org/0000-0003-1116-875X and Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2019) Using Model Checking in the Design of a Sensor Network Protocol. In: 26th Automated Reasoning Workshop (ARW 2019), London, UK, 02-03 Sep 2019, pp. 17-18.

Giaquinta, Ruben, Hoffmann, Ruth, Ireland, Murray ORCID logoORCID: https://orcid.org/0000-0001-9091-7071, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Norman, Gethin ORCID logoORCID: https://orcid.org/0000-0001-9326-4344 (2018) Strategy Synthesis for Autonomous Agents Using PRISM. In: 10th NASA Formal Methods Symposium (NFM 2018), Newport News, VA, USA, 17-19 Apr 2018, pp. 220-236. ISBN 9783319779348 (doi: 10.1007/978-3-319-77935-5_16)

Peng, Zhaoguang, Lu, Yu ORCID logoORCID: https://orcid.org/0000-0002-7799-9794 and Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2016) Uncertainty Analysis of Phased Mission Systems with Probabilistic Timed Automata. In: 7th IEEE International Conference on Prognostics and Health Management (PHM 2016), Ottawa, Canada, 20-22 June 2016, ISBN 9781509003822 (doi: 10.1109/ICPHM.2016.7542823)

Macdonald, Craig ORCID logoORCID: https://orcid.org/0000-0003-3143-279X, McCreesh, Ciaran, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Prosser, Patrick ORCID logoORCID: https://orcid.org/0000-0003-4460-6912 (2015) Constructing sailing match race schedules: round-robin pairing lists. In: 21st International Conference on Principles and Practice of Constraint Programming (CP 2015), Cork, Ireland, 31 Aug -04 Sep 2015, pp. 671-686. ISBN 9783319232188 (doi: 10.1007/978-3-319-23219-5_46)

Codish, Michael, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Frank, Michael and Itzhakov, Avraham (2015) Solving graph coloring problems with abstraction and symmetry. In: Fifth International Workshop on the Cross-Fertilization Between CSP and SAT, Cork, Ireland, 31 Aug 2015,

Lu, Yu ORCID logoORCID: https://orcid.org/0000-0002-7799-9794, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Johnson, Christopher ORCID logoORCID: https://orcid.org/0000-0002-1052-9851, Peng, Zhaoguang and Zhao, Tingdi (2015) Availability analysis of satellite positioning systems for aviation using the prism model checker. In: 17th IEEE International Conference on Computational Science and Engineering (CSE 2014), Chengdu, China, 19-21 Dec 2014, pp. 704-713. (doi: 10.1109/CSE.2014.148)

Lu, Yu ORCID logoORCID: https://orcid.org/0000-0002-7799-9794, Peng, Zhaoguang, Miller, Alice ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Zhao, Tingdi and Johnson, Chris ORCID logoORCID: https://orcid.org/0000-0002-1052-9851 (2014) Timed Fault Tree Models of the China Yongwen Railway Accident. In: 8th Asia Modelling Symposium (AMS 2014), Taipei, Taiwan, 23-25 Sep 2014, pp. 128-133. ISBN 9781479964864 (doi: 10.1109/AMS.2014.34)

Codish, M., Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Prosser, P. ORCID logoORCID: https://orcid.org/0000-0003-4460-6912 and Stuckey, A. (2013) Breaking Symmetries in Graph Representation. In: International Joint Conference on Artificial Intelligence, Beijing, China, 3-9 Aug 2013,

Kirwan, R. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2013) Formal proof of abstraction for agent-based learning systems. In: 20th Workshop on Automated Reasoning ARW 2013, Dundee, UK, 11-12 Apr 2013,

Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Kirwan, R., Porr, B. ORCID logoORCID: https://orcid.org/0000-0001-8157-998X and Di Prodi, P. (2013) Model checking for improved adaptive behaviour. In: Proceedings of the Institution of Engineering and Technology Conference on Control and Automation, Birmingham, England, 4-5 Jun 2013,

Peng, Z., Lu, Y. ORCID logoORCID: https://orcid.org/0000-0002-7799-9794, Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717, Johnson, C. ORCID logoORCID: https://orcid.org/0000-0002-1052-9851 and Zhao, T. (2013) A probabilistic model checking approach to analysing reliability, availability, and maintainability of a single satellite system. In: 7th European Modelling Symposium (EMS2013), Manchester, England, 20-22 Nov 2013, pp. 611-616. (doi: 10.1109/EMS.2013.102)

Andrei, O. ORCID logoORCID: https://orcid.org/0000-0002-1306-0219, Calder, M. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2012) Role-Based Interface Automata. In: 4th International Workshop on Foundations of Interface Technologies, Tallinn, Estonia, 25 Mar 2012,

Kirwan, R. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2010) Modelling multi-agent systems. In: Automated Reasoning Workshop 2010 Bridging the Gap between Theory and Practice ARW 2010, Harrow, UK, 30-31 Mar 2010, pp. 18-19.

Power, C. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2010) An approach to probabilistic symmetry reduction. In: Automated Reasoning Workshop 2010 Bridging the Gap between Theory and Practice ARW 2010, Harrow, UK, 30-31 Mar 2010, pp. 32-33.

Ripon, S. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2010) Verification of a symmetry detection technique using PVS. In: 10th International Workshop on Automated Verification of Critical Systems (AVoCS'2010), Düsseldorf, Germany, September 21-23, 2010,

Donaldson, A.F., Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Parker, D. (2009) Language-level symmetry reduction for probabilistic model checking. In: 6th International Conference on the Quantitative Evaluation of Systems, Budapest, 13-16 Sept 2009, pp. 289-298. (doi: 10.1109/QEST.2009.21)

Ripon, S., Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Donaldson, S. (2009) A semantic embedding of Prolema-Lite in PVS. In: Ninth International Workshop on Automated Verification of Critical Systems (AVOCS 09), Swansea, Wales, 23-25 Sep 2009,

Power, C. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2008) Prism2Promela. In: Fifth International Conference on Quantitative Evaluation of Systems, 2008. QEST '08, St. Malo, France, 14-17 Sep 2008, pp. 79-80. ISBN 978-0-7695-3360-5 (doi: 10.1109/QEST.2008.20)

Donaldson, A. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2007) Symmetry reduction techniques for explicit-state model checking. In: First International Symmetry Conference, Edinburgh, UK, 14-17 Jan 07, pp. 41-45.

Donaldson, A.F. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2007) Extending symmetry reduction techniques to a realistic model of computation. In: 6th International Workshop on Automated Verification of Critical Systems AVoCS, Nancy, France, 18-19 Sep 2006,

Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Donaldson, A.F. (2007) Symmetry reduction methods for model checking. In: Automated Reasoning Workshop 2007, London, UK, 19-20 Apr 2007,

Ballarini, P. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2006) Model checking medium access control for sensor networks. In: Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation ISoLA 2006, Paphos, Cyprus, 15-19 November 2006, pp. 255-262. (doi: 10.1109/ISoLA.2006.16)

Donaldson, A.F. and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2005) Symmetry reduction for probabilistic systems. In: The 12th Workshop on Automated Reasoning: Bridging the Gap Between Theory and Practice, Edinburgh, UK, 29-30 Jul 2005, pp. 17-18.

Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 (2005) A generic approach for the automatic verification of featured, parameterised systems. In: International Workshop on Feature Interactions in Telecommunications and Software Systems, Leicester, UK, 28-30 June 2005, pp. 217-235. ISBN 158603524X

Calder, M. and Miller, A. (2004) An automatic abstraction technique for verifying featured, parameterised systems. In: ISOLA: International Symposium on Leveraging Applications of Formal Methods, Cyprus, Greece, 30 Oct - 2 Nov 2004, pp. 227-234.

Donaldson, A., Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 (2004) Comparing the use of symmetry in constraint processing and model checking. In: 4th International Workshop on Symmetry and Constraint Satisfaction Problems, Toronto, Ontario, Canada, 27 Sep 2004, pp. 18-25.

Gregory, P., Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Prosser, P. ORCID logoORCID: https://orcid.org/0000-0003-4460-6912 (2004) Solving the rehearsal problem with planning and with model checking. In: Workshop on Modelling and Solving Problems with Constraints, Valencia, Spain, 22 Aug 2004, pp. 157-171.

Calder, M. and Miller, A. (2003) Generalising feature interactions in email. In: International Workshop on Feature Interactions in Telecommunications and Software Systems VII, Ottawa, Canada, 11-13 June 2003, pp. 187-205. ISBN 1586033484

Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 and Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 (2003) An application of abstraction and induction techniques to degenerating systems of processes. In: International Workshop on Model-Checking for Dependable Software-Intensive Systems, San Francisco, CA, USA, 22-25 Jun 2003, W75-W79.

Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2002) Five ways to use induction and symmetry in the verification of networks of processes by model-checking. In: Second Workshop on Automated Verification of Critical Systems (AVoCS 2002), April 2002, pp. 29-42.

Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (2002) Automatic verification of any number of concurrent, communicating processes. In: 17th IEEE International Conference on Automated Software Engineering, Edinburgh, 23-27 September, pp. 227-230. ISBN 0769517366 (doi: 10.1109/ASE.2002.1115017)

Calder, M. ORCID logoORCID: https://orcid.org/0000-0001-5033-7232 and Miller, A. ORCID logoORCID: https://orcid.org/0000-0002-0941-1717 (1998) Analysing a basic call protocol using Promela/XSpin. In: 4th Workshop on Automata Theoretic Verification with the SPIN Model Checker (SPIN '98), Paris, France, 2 Nov 1998, pp. 1-12.

This list was generated on Sat Jun 14 10:15:00 2025 BST.

Grants

Combinatorial Solutions for Maximum Allocations. Leverhulme Trust Fellowship, June 2024 - June2025.

M4 Secure: Making Memory Management More Secure (M4Secure), 2023-2026, CoI, EPSRC Grant EP/X037525/1

Capturing and Assuring System Requirements (CAeSaR), April 2022-March 2023, University of Glasgow PI, with D-RisQ Ltd and Herriot-Watt University.

Consent Verification in Autonomous Systems, July 2021 - July 2022, CoI, UKRI TAS Hub pump priming fund, £110,000. 

 

UKRI Trustworth Autonomous Systems Node in Governance and Regulation - "Good Governance by Design", November 2020 - April 2024, CoI, EPSRC Grant EP/V026607/1, £2.7 million.

 

Assurance and Resilience of Digital Twins in Critical Systems, October 2020 - September 2025, PI, EPSRC/DSTL Industrial Case Award.

 

Software for Red Blood Cell prediction, June 2020 - November 2020, PI, EPSRC Impact Acceleration Account (IAA), £22, 400.

 

Red Blood Cell modelling, September 2019 - January 2020.

PI, EPSRC Impact Acceleration Account (IAA), £1500.

 

Collaboration Seeding, June 2017 - June 2019:

PI, EPSRC Impact Acceleration Account (IAA), £2950.

 

Formal verification for autonomous vehicles, Aug 2016 - Mar 2016:

PI, EPSRC Institutional Scholarship Fund (ISF), £46,925.

 

UAV demonstrator for verified models of autonomous decision making, Feb 2016 - Mar 2016:

PI, EPSRC Institutional Scholarship Fund (ISF), £2,870.

 

Runtime verification of autonomous agents, Aug 2015 - Jan 2016:

PI, EPSRC Institutional Scholarship Fund (ISF), £26,207.

 

Advanced Symmetry reduction techniques for Model Checking, Jun 2007 -- May 2010:

PI, EPSRC grant no. EP/E032354/1, £210,000.

 

Verifying Interoperability Requirements in Pervasive systems, Jul 2008 -- Jun 2012:

Co-I, EPSRC grant no. EP/F033206/1, £480,000.

 

Design, Implementation and Adaption of Sensor Networks through Multi-dimensional Co-design, Oct 2005 -- Sep 2008:

Co-I, EPSRC grant no. EP/C014774/1, £260,000.

 

Verification of Concurrent Processes using Model Checking and Mathematical Analysis Techniques, Apr 2005 -- May 2007:

PI, Nuffield Foundation grant no. NAL/00968/G, £4,400$.

 

Mathematical Techniques applied to Verification tools, Mar 2005 -- Feb 2006:

PI, University of Glasgow John Robertson Bequest, grant no. JR05/14, £1000.

 

Model Checking Concurrent, Similar Processes with very large state spaces, Aug 2001--Jul 2004:

Co-author and named Research Fellow, EPSRC grant no. GR/R39122/01, £188,000.

 

Modelling and Analysing Telecommunications Software, Aug 1998--Jul 2001:

Daphne Jackson Fellowship.

Supervision

Douglas Fraser (in progress) - `Formal methods for the verification of Digital Twins' 

Ivaylo Valkov (in progress) - `Formal methods for sensor systems'

Christopher Chander (in progress) - `Model checking for trustworthy real-time decision-makng for autonomous vehicles'

William Kavanagh (graduated ) - `Model checking for game design and analysis'. 

Craig Reilly (in progress) - `Symmetry for Combinatorial Search'.

Yu Lu (graduated 2016)  - `Probabilistic Verication of Satellite Systems for Mission Critical Applications'.

Ryan Kirwan (graduated 2014) - `Applying Model Checking to Agent-based Learning Systems'.

Christopher Power (graduated 2012) - `Symmetry Reduction in Explicit State, Probabilistic Model Checking'.

Alastair Donaldson (graduated 2007) - `Automatic Techniques for Detecting and Exploiting Symmetry in Model Checking'.

Teaching

I teach the Masters course Algorithms and Data Structures (ADSIT).

Research datasets

Jump to: 2021 | 2020 | 2016
Number of items: 3.

2021

Davies, V. , Wandy, J., Weidt, S., van der Hooft, J., Miller, A. , Daly, R. and Rogers, S. (2021) Rapid Development of Improved Data-Dependent Acquisition Strategies. [Data Collection]

2020

Kavanagh, W. , Wallis, T. and Miller, A. (2020) RPGLite player data and lookup tables. [Data Collection]

2016

Kirwan, R., Miller, A. and Porr, B. (2016) Model checking learning agent systems using Promela with embedded C code and abstraction. [Data Collection]

This list was generated on Sat Jun 14 10:15:02 2025 BST.

Alice Miller

Professor Alice Miller on Twitter