Dr Gethin Norman
- Lecturer (Computing Science)
telephone: 0141 330 1630
email: Gethin.Norman@glasgow.ac.uk
Personal site: http://www.dcs.gla.ac.uk/people/personal/gethin/
Biography:
Dr Gethin Norman is SICSA lecturer in the School of Computing Science at the University of Glasgow and a member of the Formal Analysis, Theory and Algorithms research group. His research is within the field of formal verification with particular emphasis on the analysis of systems exhibiting probabilistic, stochastic and real-time behaviour. Interests within this field includes its application to software, security protocols and biological systems, as well as techniques for abstraction, refinement and the analysis of real-time and hybrid systems.
Previously he obtained a degree in mathematics from the University of Oxford and a PhD in computer science from the University of Birmingham. Between 1998 and 2007 he was a Research Fellow in the School of Computer Science at the University of Birmingham and from July 2007 until November 2009 was a research officer in the Oxford University Computing Laboratory.
Research Interests:
- quantitative model checking
- abstraction and refinement for probabilistic systems
- compositional probabilistic verification
- computational biology
- concurrency theory
- process algebras
- performance modelling
2013
Biro, P., and Norman, G. (2013) Analysis of stochastic matching markets. International Journal of Game Theory . ISSN 0020-7276 (doi:10.1007/s00182-012-0352-8) (In Press)
2012
Julvez, J., Kwiatkowska, M., Norman, G., and Parker, D. (2012) Evaluation of sustained stochastic oscillations by means of a system of differential equations. International Journal of Computers and Applications, 19 (2). pp. 101-111. ISSN 1206-212X
Di Pierro, A. and Norman, G., (Eds.) (2012) Quantitative Aspects of Programming Languages (QAPL 2010). Series: Theoretical Computer Science. Elsevier.
Kwiatkowska, M., Norman, G., and Parker, D. (2012) Probabilistic verification of Herman's self-stabilisation algorithm. Formal Aspects of Computing, 24 (4-6). pp. 661-670. ISSN 0934-5043 (doi:10.1007/s00165-012-0227-6)
2011
Hahn, E. M., Norman, G., Parker, D., Wachter, B., and Zhang, L. (2011) Game-based abstraction and controller synthesis for probabilistic Hybrid Systems. In: QEST 2011: 8th International Conference on Quantitative Evaluation of SysTems, 5-8 September 2011 , Aachen, Germany.
Massink, M. and Norman, G., (Eds.) (2011) Proceedings 9th Workshop on Quantitative Aspects of Programming Languages (QAPL'11), Saarbrücken, Germany, 1-3 April 2011. Series: Electronic Proceedings in Theoretical Computer Science. Open Publishing Association.
Forejt, V., Kwiatkowska, M., Norman, G., and Parker, D. (2011) Automated verification techniques for probabilistic systems. In: Formal Methods for Eternal Networked Software Systems 11th International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM 2011, June 13-18, 2011, Bertinoro, Italy.
Forejt, V., Kwiatkowska, M., Norman, G., Parker, D., and Qu, H. (2011) Quantitative multi-objective verification for probabilistic systems. In: Tools and Algorithms for the Construction and Analysis of Systems (TACS 2011), 26 March - 3 April 2011, Saarbrücken, Germany.
Júlvez, J., Kwiatkowska, M., Norman, G., and Parker, D. (2011) A systematic approach to evaluate sustained stochastic oscillations. In: ISCA 3rd International Conference on Bioinformatics and Computational Biology (BICoB'11), July 18-21, 2011, Monte Carlo Resort, Las Vegas, Nevada, USA.
Kwiatkowska, M., Norman, G., and Parker, D. (2011) PRISM 4.0: verification of probabilistic real-time systems. Lecture Notes in Computer Science, 6806 . pp. 585-591. ISSN 0302-9743 (doi:10.1007/978-3-642-22110-1_47)
Kwiatkowska, M., Norman, G., and Parker, D. (2011) Probabilistic model checking for systems biology. In: Iyengar, M.S. (ed.) Symbolic Systems Biology: Theory and Methods. Jones and Bartlett, Sudbury, Mass., USA. ISBN 9780763753702
2010
Di Pierro, A. and Norman, G., (Eds.) (2010) Proceedings 8th Workshop on Quantitative Aspects of Programming Languages (QAPL'10). Series: Electronic Proceedings in Theoretical Computer Science (EPTCS). EPTCS.
Duflot, M., Kwiatkowska, M., Norman, G., Parker, D., Peyronnet, S., Picaronny, C., and Sproston, J. (2010) Practical applications of probabilistic model checking to communication protocols. In: Gnesi, S. and Margaria, T. (eds.) FMICS Handbook on Industrial Critical Systems. IEEE Computer Society Press. (In Press)
Forejt, V., Kwiatkowska, M., Norman, G., and Trivedi, A. (2010) Expected reachability-time games. Lecture Notes in Computer Science, 6246 . pp. 122-136. ISSN 0302-9743 (doi:10.1007/978-3-642-15297-9_11)
Kattenbelt, M., Kwiatkowska, M., Norman, G., and Parker, D. (2010) A game-based abstraction-refinement framework for Markov decision processes. Formal Methods in System Design, 36 (3). pp. 246-280. ISSN 0925-9856 (doi:10.1007/s10703-010-0097-6)
Kwiatkowska, M., Norman, G., and Parker, D. (2010) Advances and challenges of probabilistic model checking. In: Proceedings. 48th Annual Allerton Conference on Communication, Control and Computing , September 29 – October 1, 2010, Allerton Retreat Center, Monticello, Illinois. (Unpublished)
Kwiatkowska, M., Norman, G., and Parker, D. (2010) A framework for verification of software with time and probabilities. Lecture Notes in Computer Science, 6246 . pp. 25-45. ISSN 0302-9743 (doi:10.1007/978-3-642-15297-9_4)
Kwiatkowska, M., Norman, G., Parker, D., and Qu, U. (2010) Assume-guarantee verification for probabilistic systems. In: Esparza, J. and Majumdar, R. (eds.) Tools and algorithms for the construction and analysis of systems : 16th international conference, TACAS 2010, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010 : proceedings. Series: Lecture Notes in Computer Science, 6015 . Springer. ISBN 9783642120015
2009
Chatzikokolakis, K., Norman, G., and Parker, D. (2009) Bisimulation for demonic schedulers. In: De Alfaro, L. (ed.) Foundations of Software Science and Computational Structures: 12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings. Series: Lecture notes in computer science (5504). Springer, pp. 318-332. ISBN 9783642005961
Jurdziński , M., Kwiatkowska, M., Norman, G., and Trivedi, A. (2009) Concavely-priced probabilistic timed automata. In: CONCUR 2009 - Concurrency Theory: 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedings. Series: Lecture notes in computer science (5710). Springer, pp. 415-430. ISBN 9783642040801
Kattenbelt, M., Kwiatkowska, M., Norman, G., and Parker, D. (2009) Abstraction refinement for probabilistic software. In: Jones, N.D. and Müller-Olm, M. (eds.) Verification, Model Checking, And Abstract Interpretation 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009 : Proceedings. Series: Lecture notes in computer science (5403). Springer, pp. 182-197. ISBN 9783540939009
Kwiatkowska, M., Norman, G., and Parker, D. (2009) PRISM: Probabilistic model checking for performance and reliability analysis. ACM SIGMETRICS Performance Evaluation Review, 36 (4). pp. 40-45. ISSN 0163-5999 (doi:10.1145/1530873.1530882)
Kwiatkowska, M., Norman, G., and Parker, D. (2009) Quantitative verification techniques for biological processes. In: Condon, A., Harel, D., Kok, J.N., Salomaa, A. and Winfree, E. (eds.) Algorithmic Bioprocesses. Series: Natural computing series . Springer, pp. 391-409. ISBN 9783540888697
Kwiatkowska, M., Norman, G., and Parker, D. (2009) Stochastic games for verification of probabilistic timed automata. In: Formal Modeling and Analysis of Timed Systems: 7th International Conference, FORMATS 2009, Budapest, Hungary, September 14-16, 2009. Proceedings. Series: Lecture Notes in Computer Science, (5813). Springer, pp. 212-227. ISBN 9783642043673
Kwiatkowska, M., Norman, G., Parker, D., and Vigliotti, M.G. (2009) Probabilistic mobile ambients. Theoretical Computer Science, 410 (12-13). pp. 1272-1303. ISSN 0304-3975 (doi:10.1016/j.tcs.2008.12.058)
Norman, G., Palamidessi, C., Parker, D., and Wu, P. (2009) Model checking probabilistic and stochastic extensions of the pi-calculus. IEEE Transactions on Software Engineering, 35 (2-3). pp. 209-223. ISSN 0098-5589 (doi:10.1109/TSE.2008.77 )
2008
Heath, J., Kwiatkowska, M., Norman, G., Parker, D., and Tymchyshyn, O. (2008) Probabilistic model checking of complex biological pathways. Theoretical Computer Science, 391 (3). pp. 239-257. ISSN 0304-3975 (doi:10.1016/j.tcs.2007.11.013)
Kattenbelt, M., Kwiatkowska, M., Norman, G., and Parker, D. (2008) Game-based probabilistic predicate abstraction in PRISM. Electronic Notes in Theoretical Computer Science, 220 (3). pp. 5-21. ISSN 1571-0661 (doi:10.1016/j.entcs.2008.11.016 )
Kwiatkowska, M., Norman, G., and Parker, D. (2008) Analysis of a gossip protocol in PRISM. ACM SIGMETRICS Performance Evaluation Review, 36 (3). pp. 17-22. ISSN 0163-5999 (doi:10.1145/1481506.1481511)
Kwiatkowska, M., Norman, G., and Parker, D. (2008) Using probabilistic model checking in systems biology. ACM SIGMETRICS Performance Evaluation Review, 34 (4). pp. 14-21. ISSN 0163-5999 (doi:10.1145/1364644.1364651)
Kwiatkowska, M., Norman, G., Parker, D., and Sproston, J. (2008) Verification of real-time probabilistic systems. In: Merz, S. and Navet, N. (eds.) Modeling and Verification of Real-Time Systems: Formalisms and Software Tools. John Wiley & Sons Ltd., pp. 249-288. ISBN 9781848210134
Roy, P., Parker, D., Norman, G., and de Alfaro, L. (2008) Symbolic Magnifying Lens Abstraction in Markov Decision Processes. In: International Conference on Quantitative Evaluation of Systems (QEST'08), 14-17 Sept. 2008 , St. Malo, France.
2007
Kwiatkowska, M., Norman, G., and Parker, D. (2007) Controller dependability analysis by probabilistic model checking. Control Engineering Practice, 15 (11). pp. 1427-1434. ISSN 0967-0661 (doi:10.1016/j.conengprac.2006.07.003)
Kwiatkowska, M., Norman, G., and Parker, D. (2007) Stochastic model checking. In: Bernardo , M. and Hillston, J. (eds.) Formal Methods for Performance Evaluation: 7th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2007, Bertinoro, Italy, May 28-June 2, 2007, Advanced Lectures. Series: Lecture notes in computer science (4486). Springer, pp. 220-270. ISBN 9783540725220
Kwiatkowska, M., Norman, G., Sproston, J., and Wang, F. (2007) Symbolic model checking for probabilistic timed automata. Information and Computation, 205 (7). 1027-1077 . ISSN 0890-5401 (doi:10.1016/j.ic.2007.01.004 )
Norman, G., Palamidessi, C., Parker, D., and Wu, P. (2007) Model checking the probabilistic pi-calculus. In: Proceedings Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007), September 17-19, 2007, Edinburgh, Scotland.
2006
Duflot, M., Kwiatkowska, M., Norman, G., and Parker, D. (2006) A formal analysis of bluetooth device discovery. International Journal on Software Tools for Technology Transfer (STTT) , 8 (6). pp. 621-632. ISSN 1433-2779 (doi:10.1007/s10009-006-0014-x)
Norman, G., and Shmatikov, V. (2006) Analysis of probabilistic contract signing. Journal of Computer Security, 14 (6). pp. 561-589. ISSN 0926-227X
Heath, J., Kwiatkowska, M., Norman, G., Parker, D., and Tymchyshyn, O. (2006) Probabilistic model checking of complex biological pathways. In: Computational Methods in Systems Biology (CMSB'06), October 18-19, 2006, Trento, Italy.
Kwiatkowska, M., Norman, G., Parker, D., and Sproston, J. (2006) Performance analysis of probabilistic timed automata using digital clocks. Formal Methods in System Design, 29 (1). pp. 33-78. ISSN 0925-9856 (doi:10.1007/s10703-006-0005-2)
Younes, H.L.S., Kwiatkowska, M., Norman, G., and Parker, D. (2006) Numerical vs. statistical probabilistic model checking. International Journal on Software Tools for Technology Transfer (STTT), 8 (3). pp. 216-228. ISSN 1433-2779 (doi:10.1007/s10009-005-0187-8)
Hinton, A., Kwiatkowska, M., Parker, D., and Norman, G. (2006) PRISM: a tool for automatic verification of probabilistic systems. Lecture Notes in Computer Science, 3920 . pp. 441-444. ISSN 0302-9743 (doi:10.1007/11691372_29)
Kwiatkowska, M., Norman, G., and Pacheco, A. (2006) Model checking expected time and expected reward formulae with random time bounds. Computers and Mathematics with Applications, 51 (2). pp. 305-316. ISSN 0898-1221 (doi:10.1016/j.camwa.2005.11.016)
Groesser, M., Norman, G., Baier, C., Ciesinski, F., Kwiatkowska, M., and Parker, D. (2006) On reduction criteria for probabilistic reward models. In: Arun-Kumar, S. and Garg, N. (eds.) Foundations of Software Technology and Theoretical Computer Science (FSTTCS'06). Series: Lecture notes in computer science (4337). Springer Verlag, pp. 309-320. ISBN 9783540499954
Kwiatkowska, M., Norman, G., and Parker, D. (2006) Game-based abstraction for Markov decision processes. In: 3rd International Conference on Quantitative Evaluation of Systems (QEST'06), 11-14 Sept 2006, Riverside, California, USA.
Kwiatkowska, M., Norman, G., and Parker, D. (2006) Symmetry reduction for probabilistic model checking. Lecture Notes in Computer Science, 4144 . pp. 234-248. ISSN 0302-9743 (doi:10.1007/11817963_23)
Kwiatkowska, M., Norman, G., Parker, D., Tymchyshyn, O., Heath , J., and Gaffney, E. (2006) Simulation and verification for computational modelling of signalling pathways. In: Perrone, L., Wieland, F.P., Liu, J., Lawson, B.J., Nicol, D.M. and Fujimoto, R.M. (eds.) Proceedings of the 2006 Winter Simulation Conference. WSC, pp. 1666-1674. ISBN 1424405009
2005
Norman, G., Parker, P., Kwiatkowska, M., and Shukla, S. (2005) Evaluating the reliability of NAND multiplexing with PRISM. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 24 (10). 1629 -1637 . ISSN 0278-0070 (doi:10.1109/TCAD.2005.852033 )
Kwiatkowska, M., Norman, G., and Parker, D. (2005) Probabilistic Model Checking and Power-Aware Computing. In: 7th International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS), September 23-24, 2005, Torino, Italy.
Norman, G., Parker, D., Kwiatkowska, M., Shukla, S., and Gupta, R. (2005) Using probabilistic model checking for dynamic power management. Formal Aspects of Computing, 17 (2). pp. 160-176. ISSN 0934-5043 (doi:10.1007/s00165-005-0062-0)
2004
Daws, C., Kwiatkowska, M., and Norman, G. (2004) Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM. International Journal on Software Tools for Technology Transfer (STTT), 5 (2). pp. 221-236. ISSN 1433-2779 (doi:10.1007/s10009-003-0118-5)
Kwiatkowska, M., Norman, G., and Parker, D. (2004) Probabilistic symbolic model checking with PRISM: a hybrid approach. International Journal on Software Tools for Technology Transfer (STTT) , 6 (2). pp. 128-142. ISSN 1433-2779 (doi:10.1007/s10009-004-0140-2)
2002
Kwiatkowska, M., Norman, G., Segala, R., and Sproston, J. (2002) Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science, 282 (1). pp. 101-150. ISSN 0304-3975 (doi:10.1016/S0304-3975(01)00046-9 )
2001
Katoen, J.P., Kwiatkowska, M., Norman, G., and Parker, D. (2001) Faster and symbolic CTMC model checking. In: de Alfaro, L. and Gilmore, S. (eds.) Process Algebra and Probabilistic Methods : Performance Modeling and Verification : Joint International Workshop. Series: Lecture notes in computer science (2165). Springer-Verlag, Berlin; New York, pp. 23-38. ISBN 9783540425564
Kwiatkowska, M., Norman, G., and Segala, R. (2001) Automated verication of a randomized distributed concensus protocol using Cadence SMV and PRISM. In: Berry, G., Common, H. and Finkel, A. (eds.) Computer Aided Verification: 13th International Conference, CAV 2001, Paris, France, July 2001 : Proceedings. Series: Lecture notes in computer science (2102). Springer-Verlag, Berlin, pp. 194-206. ISBN 9783540423454
