Professor Alice Miller
- Professor (Computing Science)
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 Deputy Head of School and a member of the School Executive. I lead the School's Athena Swan working group.
Personal site: http://www.dcs.gla.ac.uk/~alice
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
- Group Theory
- Graph Theory
Codish, M., Frank, M., Itzhakov, A. and Miller, A. (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)
Giaquinta, R., Hoffmann, R., Ireland, M. , Miller, A. and Norman, G. (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)
Hoffmann, R., Ireland, M. , Miller, A. , Norman, G. and Veres, S. (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)
Codish, M., Miller, A. , Prosser, P. and Stuckey, P. J. (2019) Constraints for symmetry breaking in graph representation. Constraints, 24(1), pp. 1-24. (doi: 10.1007/s10601-018-9294-5)
Kirwan, R., Miller, A. and Porr, B. (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)
Porr, B. , Miller, A. and Trew, A. (2019) An investigation into serotonergic and environmental interventions against depression in a simulated delayed reward paradigm. Adaptive Behavior, (doi: 10.1177/1059712319864278) (Early Online Publication)
Kavanagh, W. J. , Miller, A. , Norman, G. and Andrei, O. (2019) Balancing turn-based games with chained strategy generation. IEEE Transactions on Games, (doi: 10.1109/TG.2019.2943227) (Early Online Publication)
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.
- Kavanagh, William
Investigation into the viability of model checking to aid video game development
Craig Reilly (in progress) - `Symmetry for Combinatorial Search'.
William Kavanagh (in progress) - `Model checking for game design and analysis'.
Ivaylo Valkov (in progress) - `Formal methods for sensor systems'
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'.
I teach the level H/M course on "Modelling Reactive Systems" (MRSH/M), the Masters course in Programming (ProgIT) and the Masters course in Algorithms and Data Structures (ADSIT).