Using SPIN for Feature Interaction Analysis - A Case Study. - Muffy Calder; Alice Miller 001 (SPIN, 2001)

Automatic Verification of any Number of Concurrent, Communicating Processes. - Muffy Calder; Alice Miller 001 (ASE, 2002)

Detecting Feature Interactions: How Many Components Do We Need? - Muffy Calder; Alice Miller 001 (Objects, Agents, and Features, 2003)

Generalising Feature Interactions in Email. - Muffy Calder; Alice Miller 001 (FIW, 2003)

Using SPIN to Analyse the Tree Identification Phase of the IEEE 1394 High-Performance Serial Bus (FireWire) Protocol. - Muffy Calder; Alice Miller 001 (Formal Aspects Comput., 2003)

Verifying parametrized, featured networks by abstraction. - Muffy Calder; Alice Miller 001 (ISoLA (Preliminary proceedings), 2004)

Finding Symmetry in Models of Concurrent Systems by Static Channel Diagram Analysis. - Alastair F. Donaldson; Alice Miller 001; Muffy Calder (AVoCS, 2004)

Spin-to-Grape: A Tool for Analysing Symmetry in Promela Models. - Alastair F. Donaldson; Alice Miller 001; Muffy Calder (ARTS, 2004)

A Generic Approach for the Automatic Verification of Featured, Parameterised Systems. - Alice Miller 001; Muffy Calder (FIW, 2005)

Automatic Symmetry Detection for Model Checking Using Computational Group Theory. - Alastair F. Donaldson; Alice Miller 001 (FM, 2005)

A Computational Group Theoretic Symmetry Reduction Package for the Spin Model Checker. - Alastair F. Donaldson; Alice Miller 001 (AMAST, 2006)

Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives. - Alastair F. Donaldson; Alice Miller 001 (ATVA, 2006)

Exact and Approximate Strategies for Symmetry Reduction in Model Checking. - Alastair F. Donaldson; Alice Miller 001 (FM, 2006)

Model Checking Medium Access Control for Sensor Networks. - Paolo Ballarini; Alice Miller 001 (ISoLA, 2006)

Symmetry in temporal logic model checking. - Alice Miller 001; Alastair F. Donaldson; Muffy Calder (ACM Comput. Surv., 2006)

Extending Symmetry Reduction Techniques to a Realistic Model of Computation. - Alastair F. Donaldson; Alice Miller 001 (AVoCS, 2006)

Feature interaction detection by pairwise analysis of LTL properties - A case study. - Muffy Calder; Alice Miller 001 (Formal Methods Syst. Des., 2006)

GRIP: Generic Representatives in PRISM. - Alastair F. Donaldson; Alice Miller 001; David Parker 001 (QEST, 2007)

A template-based approach for the generation of abstractable and reducible models of featured networks. - Alice Miller 001; Muffy Calder; Alastair F. Donaldson (Comput. Networks, 2007)

An Inductive Technique for Parameterised Model Checking of Degenerative Distributed Randomised Protocols. - Douglas Graham; Muffy Calder; Alice Miller 001 (AVoCS, 2007)

Prism2Promela. - Christopher Power; Alice Miller 001 (QEST, 2008)

Preface. - Alice Miller 001; Muffy Calder (AVoCS, 2008)

Automatic Symmetry Detection for Promela. - Alastair F. Donaldson; Alice Miller 001 (J. Autom. Reason., 2008)

An automatic abstraction technique for verifying featured, parameterised systems. - Muffy Calder; Alice Miller 001 (Theor. Comput. Sci., 2008)

Language-Level Symmetry Reduction for Probabilistic Model Checking. - Alastair F. Donaldson; Alice Miller 001; David Parker 001 (QEST, 2009)

Towards Verifying Correctness of Wireless Sensor Network Applications Using Insense and Spin. - Oliver Sharma; Jonathan Lewis; Alice Miller 001; Alan Dearle; Dharini Balasubramaniam; Ronald Morrison; Joe Sventek (SPIN, 2009)

On the constructive orbit problem. - Alastair F. Donaldson; Alice Miller 001 (Ann. Math. Artif. Intell., 2009)

Towards the Verification of Pervasive Systems. - Myrto Arapinis; Muffy Calder; Louise A. Dennis; Michael Fisher 001; Philip D. Gray; Savas Konur; Alice Miller 001; Eike Ritter; Mark Ryan 001; Sven Schewe; Chris Unsworth; Rehana Yasmin (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2009)

An Introduction to Pervasive Interface Automata. - Muffy Calder; Philip D. Gray; Alice Miller 001; Chris Unsworth (FACS, 2010)

Verification of Symmetry Detection using PVS. - Shamim Ripon; Alice Miller 001 (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2010)

Diamond-free Degree Sequences - Alice Miller 001; Patrick Prosser (CoRR, 2012)

A Probabilistic Model Checking Approach to Analysing Reliability, Availability, and Maintainability of a Single Satellite System. - Zhaoguang Peng; Yu Lu 001; Alice Miller 001; Chris W. Johnson 001; Tingdi Zhao (EMS, 2013)

Breaking Symmetries in Graph Representation. - Michael Codish; Alice Miller 001; Patrick Prosser; Peter James Stuckey (IJCAI, 2013)

Formal Modeling of Robot Behavior with Learning. - Ryan F. Kirwan; Alice Miller 001; Bernd Porr; Paolo di Prodi (Neural Comput., 2013)

Availability Analysis of Satellite Positioning Systems for Aviation Using the PRISM Model Checker. - Yu Lu 001; Alice Miller 001; Chris W. Johnson 001; Zhaoguang Peng; Tingdi Zhao (CSE, 2014)

Solving Graph Coloring Problems with Abstraction and Symmetry: the Ramsey Number R(4, 3, 3)=30. - Michael Codish; Michael Frank 002; Avraham Itzhakov; Alice Miller 001 (CoRR, 2014)

Formal modelling and quantitative analysis of satellite navigation systems. - Zhaoguang Peng; Yu Lu 001; Alice Miller 001; Chris W. Johnson 001; Tingdi Zhao (CoRR, 2014)

Constructing Sailing Match Race Schedules: Round-Robin Pairing Lists. - Craig Macdonald; Ciaran McCreesh; Alice Miller 001; Patrick Prosser (CP, 2015)

How reliable is satellite navigation for aviation? Checking availability properties with probabilistic verification. - Yu Lu 001; Zhaoguang Peng; Alice Miller 001; Tingdi Zhao; Chris W. Johnson 001 (Reliab. Eng. Syst. Saf., 2015)

Towards the Automated Verification of Weibull Distributions for System Failure Rates. - Yu Lu 001; Alice A. Miller; Ruth Hoffmann; Christopher W. Johnson 001 (FMICS-AVoCS, 2016)

Uncertainty analysis of phased mission systems with probabilistic timed automata. - Zhaoguang Peng; Yu Lu 001; Alice Miller 001 (ICPHM, 2016)

Autonomous Agent Behaviour Modelled in PRISM - A Case Study. - Ruth Hoffmann; Murray L. Ireland; Alice Miller 001; Gethin Norman; Sandor M. Veres (SPIN, 2016)

Computing the Ramsey number R(4, 3, 3) using abstraction and symmetry breaking. - Michael Codish; Michael Frank 002; Avraham Itzhakov; Alice Miller 001 (Constraints An Int. J., 2016)

A Continuous-Time Model of an Autonomous Aerial Vehicle to Inform and Validate Formal Verification Methods. - Murray L. Ireland; Ruth Hoffmann; Alice Miller 001; Gethin Norman; Sandor M. Veres (CoRR, 2016)

Model checking learning agent systems using Promela with embedded C code and abstraction. - Ryan F. Kirwan; Alice Miller 001; Bernd Porr (Formal Aspects Comput., 2016)

Risk Assessment of Railway Transportation Systems using Timed Fault Trees. - Zhaoguang Peng; Yu Lu 001; Alice Miller 001; Chris W. Johnson 001; Tingdi Zhao (Qual. Reliab. Eng. Int., 2016)

Formal Specification and Quantitative Analysis of a Constellation of Navigation Satellites. - Zhaoguang Peng; Yu Lu 001; Alice Miller 001; Tingdi Zhao; Chris W. Johnson 001 (Qual. Reliab. Eng. Int., 2016)

Strategy Synthesis for Autonomous Agents Using PRISM. - Ruben Giaquinta; Ruth Hoffmann; Murray L. Ireland; Alice Miller 001; Gethin Norman (NFM, 2018)

Constraints for symmetry breaking in graph representation. - Michael Codish; Alice Miller 001; Patrick Prosser; Peter J. Stuckey (Constraints An Int. J., 2019)

An investigation into serotonergic and environmental interventions against depression in a simulated delayed reward paradigm. - Bernd Porr; Alice Miller 001; Alex Trew (Adapt. Behav., 2020)

Collaborative models for autonomous systems controller synthesis. - Douglas Fraser; Ruben Giaquinta; Ruth Hoffmann; Murray Ireland; Alice Miller 001; Gethin Norman (Formal Aspects Comput., 2020)

GBRAMP: A generalized backtracking regularized adaptive matching pursuit algorithm for signal reconstruction. - Mojisola Grace Asogbon; Yu Lu 001; Oluwarotimi Williams Samuel; Liwen Jing; Alice A. Miller; Guanglin Li 001; Kelvin Kian Loong Wong (Comput. Electr. Eng., 2021)

Gameplay Analysis of Multiplayer Games with Verified Action-Costs. - William Kavanagh; Alice Miller 001 (Comput. Games J., 2021)

Designing a mobile game to generate player data - lessons learned. - William Wallis; William Kavanagh; Alice Miller 001; Tim Storer (CoRR, 2021)

Simulation and Model Checking for Close to Realtime Overtaking Planning. - Daumantas Pagojus; Alice Miller 001; Bernd Porr; Ivaylo Valkov (FMAS, 2021)

Breakout Group Allocation Schedules and the Social Golfer Problem with Adjacent Group Sizes. - Alice Miller 001; Matthew Barr; William Kavanagh; Ivaylo Valkov; Helen C. Purchase (Symmetry, 2021)

Balancing Turn-Based Games With Chained Strategy Generation. - William Kavanagh; Alice Miller 001; Gethin Norman; Oana Andrei (IEEE Trans. Games, 2021)

Mix-and-Match MCQs: Four for the Price of One. - Helen C. Purchase; Alice A. Miller (ITiCSE (2), 2022)

Model Checking for Closed-Loop Robot Reactive Planning. - Christopher Chandler; Bernd Porr; Alice Miller 001; Giulia Lafratta (FMAS@iFM, 2023)

Feasibility assessments of a dynamical approach to compartmental modelling on graphs: Scaling limits and performance analysis. - Ethan Hunter; Jessica A. Enright; Alice Miller 001 (Theor. Comput. Sci., 2023)

Synchronisation in Language-Level Symmetry Reduction for Probabilistic Model Checking. - Ivaylo Valkov; Alastair F. Donaldson; Alice Miller 001 (SPIN, 2024)

Homeostatic motion planning with innate physics knowledge. - Giulia Lafratta; Bernd Porr; Christopher Chandler; Alice Miller 001 (CoRR, 2024)

Closed-loop multi-step planning with innate physics knowledge. - Giulia Lafratta; Bernd Porr; Christopher Chandler; Alice Miller 001 (CoRR, 2024)

Model checking with memoisation for fast overtaking planning. - Alice Miller 001; Bernd Porr; Ivaylo Valkov; Douglas Fraser; Daumantas Pagojus (Sci. Comput. Program., 2025)