Dr Alice Miller

  • Senior Lecturer (Computing Science)

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

Research interests

Personal site: http://www.dcs.gla.ac.uk/~alice

Formal verification and model checking

Biography:
Dr. Alice Miller is a Senior Lecturer and member of the Formal Analysis, Theory and Algorithms Group within the School of Computing Science at the University of Glasgow. Previously, Dr Miller has worked at the universities of Western Australia, East Anglia and Stirling and was a Daphne Jackson Fellow. She received her Ph.D. in Number Theory from the University of East Anglia in 1989, under the supervision of Prof. Graeme Everest. Prior to this she received a First Class Honours Degree in Mathematics from the University of East Anglia. She is a member of the London Mathematical Society and the IET, and is a Chartered Engineer.

Research Interests:
- Modelling and Verification
- Abstraction and Symmetry Reduction
- Combinatorics
- Group Theory

Supervision

Publications

List by: Type | Date

Jump to: 2016 | 2015 | 2014 | 2013 | 2012 | 2011 | 2010 | 2009 | 2008 | 2007 | 2006 | 2005 | 2004 | 2003 | 2002 | 2001 | 1998 | 1996 | 1994 | 1991
Number of items: 75.

2016

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)

Lu, Y., Miller, A. A. , Hoffmann, R. and Johnson, C. W. (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, Z., Lu, Y. and Miller, A. (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, 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)

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)

Peng, Z., Lu, Y., Miller, A. , Tingdi, Z. and Johnson, C. (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, Z., Lu, Y., Miller, A. , Johnson, C. and Zhao, T. (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)

Codish, M., Frank, M., Itzhakov, A. and Miller, A. (2016) Computing the Ramsey Number R(4,3,3) Using Abstraction and Symmetry Breaking. 13th International Conference on Integration of Artificial Intelligence (AI) and Operations Research (OR) techniques in Constraint Programming, Banff, Canada, 29 May - 1 Jun 2016. (Accepted for Publication)

2015

Lu, Y., Peng, Z., Miller, A. A. , Zhao, T. and Johnson, C. W. (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, C., McCreesh, C., Miller, A. and Prosser, P. (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, M., Miller, A. , Frank, M. and Itzhakov, A. (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, Y., Miller, A. , Johnson, C., Peng, Z. and Zhao, T. (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, Y., Peng, Z., Miller, A. , Zhao, T. and Johnson, C. (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, E. K., Winfield, J. M., Adam, D., Miller, A. A. , Carr, R. H., Eaglesham, A. and Lennon, D. (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, R., Miller, A. , Porr, B. 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. , Prosser, P. 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. (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. , Kirwan, R., Porr, B. 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., Miller, A. , Johnson, C. 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. and Miller, A. (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., Calder, M. and Miller, A. (2012) Role-based interface automata. In: 4th International Workshop on Foundations of Interface Technologies, Tallinn, Estonia, 25 Mar 2012,

Calder, M., Gray, P., Miller, A. 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. (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. and Prosser, P. (2012) Diamond-free degree sequences. Acta Universitatis Sapientiae, Informatica, 4(2), pp. 189-200.

Miller, A. (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. (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. (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. (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. (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. (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. 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. and Miller, A. (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. and Calder, M. (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. (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. 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., 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. (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. and Miller, A. (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. (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. (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. (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. 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. 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. (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. (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, A. and Miller, A. (2006) Symmetry reduction for probabilistic model checking using generic representatives. Automated Technology For Verification and Analysis, Proceedings, 4218, pp. 9-23.

Miller, A. and Cutts, Q. (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. (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)

Donaldson, A.F. and Miller, A. (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. (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. and Calder, M. (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

Miller, A., Prosser, P. 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.

2004

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. (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. and Calder, M. (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. and Prosser, P. (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. and Calder, M. (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. and Miller, A. (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. and Miller, A. (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.

2001

Calder, M. and Miller, A. (2001) Using SPIN for feature interaction analysis - a case study. Lecture Notes in Computer Science, 2057, pp. 143-162.

Miller, A. (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. and Miller, A. (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. (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. 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. (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 Tue Jun 27 11:24:01 2017 BST.
Number of items: 75.

Articles

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)

Lu, Y., Miller, A. A. , Hoffmann, R. and Johnson, C. W. (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, 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)

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)

Peng, Z., Lu, Y., Miller, A. , Tingdi, Z. and Johnson, C. (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, Z., Lu, Y., Miller, A. , Johnson, C. and Zhao, T. (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, Y., Peng, Z., Miller, A. A. , Zhao, T. and Johnson, C. W. (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, E. K., Winfield, J. M., Adam, D., Miller, A. A. , Carr, R. H., Eaglesham, A. and Lennon, D. (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, R., Miller, A. , Porr, B. 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., Gray, P., Miller, A. 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. and Prosser, P. (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. (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. and Miller, A. (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. and Calder, M. (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., 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. (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. and Miller, A. (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, A. and Miller, A. (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. (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. and Miller, A. (2001) Using SPIN for feature interaction analysis - a case study. Lecture Notes in Computer Science, 2057, pp. 143-162.

Miller, A. (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. (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. 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. (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. and Miller, A. (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. (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. (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. (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. 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. (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. and Cutts, Q. (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. (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., Prosser, P. 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.

Research Reports or Papers

Miller, A. (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

Codish, M., Frank, M., Itzhakov, A. and Miller, A. (2016) Computing the Ramsey Number R(4,3,3) Using Abstraction and Symmetry Breaking. 13th International Conference on Integration of Artificial Intelligence (AI) and Operations Research (OR) techniques in Constraint Programming, Banff, Canada, 29 May - 1 Jun 2016. (Accepted for Publication)

Conference Proceedings

Peng, Z., Lu, Y. and Miller, A. (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, C., McCreesh, C., Miller, A. and Prosser, P. (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, M., Miller, A. , Frank, M. and Itzhakov, A. (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, Y., Miller, A. , Johnson, C., Peng, Z. and Zhao, T. (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, Y., Peng, Z., Miller, A. , Zhao, T. and Johnson, C. (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. , Prosser, P. 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. (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. , Kirwan, R., Porr, B. 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., Miller, A. , Johnson, C. 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., Calder, M. and Miller, A. (2012) Role-based interface automata. In: 4th International Workshop on Foundations of Interface Technologies, Tallinn, Estonia, 25 Mar 2012,

Kirwan, R. and Miller, A. (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. (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. (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. 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. 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. (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. (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. (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. 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. (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. (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. and Calder, M. (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. and Calder, M. (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. and Prosser, P. (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. and Calder, M. (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. and Miller, A. (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. and Miller, A. (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. and Miller, A. (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 Tue Jun 27 11:24:01 2017 BST.