Dr Gethin Norman Scottish Informatics and Computer Science Alliance (SICSA) Senior Lecturer in the School of Computing Science at the University of Glasgow. Member of the formal methods research group which is part of the Formal Analysis, Theory and Algorithms research section. Co-leader of SICSA's Modelling and Abstraction research theme between 2012-16. Currently the Deputy Head of the School. Senior Research Fellow at the Department of Computer Science at the University of Oxford working on the FUN2MODEL: From FUNction-based TO MOdel-based automated probabilistic reasoning for DEep Learning research project.

My research is within the field of formal verification with emphasis on quantitative formal methods, particularly models and algorithms for systems exhibiting real-time and probabilistic behaviour. My interests within this field includes its application to software, security protocols and biological systems, as well as techniques for abstraction and refinement, compositional analysis and using game theory. For further details see my publication page.

If you are interested completing a PhD related to my research, then please contact me. You can find information about the application process here.

Biography

I 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 I was a Research Fellow in the School of Computer Science at the University of Birmingham working on the EPSRC funded projects: "Automatic Verification of Randomized Distributed Algorithms" (rated outstanding), "Verification of Quality of Service Properties in Timed Systems" (rated outstanding) and "Probabilistic Model Checking of Mobile Ad Hoc Network Protocols". In addition during this time I contributed to the "A Future Of Reliable Wireless Ad-hoc networks of Roaming Devices (FORWARD) project" which was part of the Next Wave Technologies and Markets, and was a team member of the "Predictive modelling of signalling pathways via probabilistic model checking with PRISM" project (funded by Microsoft Research Cambridge).

From July 2007 until November 2009, I was a research officer in the Oxford University Computing Laboratory working on the EPSRC funded project "UbiVal: Fundamental Approaches to Validation of Ubiquitous Computing Applications and Infrastructures" (EPSRC Research Grant EP/D077273/1) which is a collaboration between University of Birmingham, Oxford, UCL and Imperial College.

In November 2009, I became a lecturer in the School of Computing Science at the University of Glasgow and in July 2017 a senior lecturer.

I am also one of the principal developers for the probabilistic verification tool PRISM.

Publications

See an online list of publications or find me on DBLP, google scholar, scopus, ORCID or microsoft academic.

Activities

Editorial boards

• Entropy

Steering Committees

• Conference on the Quantitative Evaluation of Systems (QEST) 2012-14, 2016-18, 2019-2024
• Workshop on Quantitative Aspects of Programming Languages (QAPL) 2010-2018

Program Committees

• Twentieth European Conference on Multi-Agent Systems (EUMAS'23)
• Twentieth International Conference on the Quantitative Evaluation of Systems (QEST 2023)
• Thirty Seventh Conference on Artificial Intelligence (AAAI 2023)
• Twentieth International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2022) (Publicity Chair)
• Nineteenth International Conference on the Quantitative Evaluation of Systems (QEST 2022)
• Flavors of Uncertainty in Verification, Planning, and Optimization (FUNCTION 2021) (Workshop Chair)
• Seventh International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT (SNR 2021)
• Eighteenth International Conference on the Quantitative Evaluation of Systems (QEST 2021)
• Twenty Forth ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2021)
• Forty Eighth International Colloquium on Automata, Languages, and Programming (ICALP 2021) (Workshop Chair and SafeToc advocate)
• Eighteenth International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2020)
• Seventeenth International Conference on the Quantitative Evaluation of Systems (QEST 2020)
• Twenty Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020)
• First Workshop on Formal Techniques for Dependable Autonomous Systems (FT4DAS 2019)
• Sixteenth International Conference on the Quantitative Evaluation of Systems (QEST 2019) (General Chair)
• Twenty Third International Symposium on Formal Methods (FM 2019)
• The Federated Logic Conference 2018 (FLoC 2018) (Workshops Chair)
• Fifteenth International Conference on the Quantitative Evaluation of Systems (QEST 2018)
• Fourteenth International Conference on the Quantitative Evaluation of Systems (QEST 2017)
• Third Graphs as Models Workshop (GaM 2017)
• Seventh International Workshop on Static Analysis and Systems Biology (SASB 2016)
• Twenty Seventh International Conference on Concurrency Theory (CONCUR 2016)
• Sixth International Workshop on Static Analysis and Systems Biology (SASB 2015)
• Thirteenth Workshop on Quantitative Aspects of Programming Languages (QAPL 2015)
• Eighth Workshop on Membrane Computing and Biologically Inspired Process Calculi (MeCBIC 2014)
• Eleventh International Conference on the Quantitative Evaluation of Systems (QEST 2014) (PC chair)
• 19th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2014)
• Twelfth Workshop on Quantitative Aspects of Programming Languages (QAPL 2014)
• Twenty Second International Conference on Parallel, Distributed, and Network-Based Processing (Track: Advances in High-Performance Bioinformatics, Systems and Synthetic Biology ) (PDP 2014)
• Seventh Workshop on Membrane Computing and Biologically Inspired Process Calculi (MeCBIC 2013)
• Fourth International Workshop on Static Analysis and Systems Biology (SASB 2013)
• Nineteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013)
• Tenth International Conference on the Quantitative Evaluation of Systems (QEST 2013)
• Eleventh Workshop on Quantitative Aspects of Programming Languages (QAPL 2013)
• Joint Workshop On Compositional Modelling And Analysis Of Quantitative Systems (MLQA 2012)
• Sixth Workshop on Membrane Computing and Biologically Inspired Process Calculi (MeCBIC 2012)
• Third International Workshop on Static Analysis and Systems Biology (SASB 2012)
• Eleventh International Workshop on Parallel and Distributed Methods in Verification (PDMC 2012)
• Tenth Workshop on Quantitative Aspects of Programming Languages (QAPL 2012)
• Third International Workshop on Computer Science to Systems Biology (CS2Bio12)
• Fifth Workshop on Membrane Computing and Biologically Inspired Process Calculi (MeCBIC 2011)
• Second International Workshop on Static Analysis and Systems Biology (SASB 2011)
• Workshop on Formal Methods for Pervasive Systems (Pervasive@FM2011)
• Eighth International Conference on the Quantitative Evaluation of Systems (QEST 2011) (tutorial chair)
• Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL 2011) (PC chair)
• Second International Workshop on Computer Science to Systems Biology (CS2Bio11)
• Mediation Services in Computing Environments (MeSC), track of 26th ACM Symposium on Applied Computing
• First International Workshop on Computer Science to Systems Biology (CS2Bio10)
• Second International Workshop on High Performance Computational Systems Biology (HiBi 2010)
• Eighth Workshop on Quantitative Aspects of Programming Languages (QAPL 2010) (PC chair)
• Seventh International Conference on the Quantitative Evaluation of Systems (QEST 2010)
• First International Workshop on High Performance Computational Systems Biology (HiBi 2009)
• Seventh Workshop on Quantitative Aspects of Programming Languages (QAPL 2009)
• Fifteenth International Workshop on Expressiveness in Concurrency (EXPRESS 2008)
• Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007
• Fifth International Conference on Computational Methods in Systems Biology (CMSB 2007)
• Third International Conference on the Quantitative Evaluation of Systems (QEST 2006)
• Second International Workshop on Practical Applications of Stochastic Modelling (PASM 2005)
• Second International Conference on the Quantitative Evaluation of Systems (QEST 2005)
• First International Workshop on Practical Applications of Stochastic Modelling (PASM 2004)

Collaborators

• Marta Kwiatkowska (Oxford University Computing Laboratory)
• Dave Parker (University of Birmingham)
• Mark Kattenbelt (Oxford University Computing Laboratory)
• Jeremy Sproston (Universita degli Studi di Torino)
• Roberto Segala (Universita di Verona)
• Luca de Alfaro (University of California, Santa Cruz)
• Joost-Pieter Katoen (RWTH Aachen University)
• Christel Baier (TU Dresden)
• Conrado Daws (University of Nijmegen)
• Antonio Pacheco (Instituto Superior Tecnico Lisboa)
• Markus Siegle (Universitat der Bundeswehr Munchen)
• Holger Hermanns (Saarland University)
• Sylvain Peyronnet (LRI)
• Haakan L. S. Younes (Carnegie Mellon University)
• Vitaly Shmatikov (University of Texas at Austin)
• Rajesh Gupta (University of California, Irvine)
• Sandeep Shukla (Virginia Tech)
• Marie Duflot (Universite Paris XII)
• John Heath (University of Birmingham)
• Catuscia Palamidessi (INRIA Futurs Saclay and LIX)
• Peng Wu (UCL)
• Kostas Chatzikokolakis (Ecole Polytechnique Paris)
• Ashutosh Trivedi (Indian Institute of Technology Bombay)
• Marcin Jurdzinski (University of Warwick)
• Vojtech Forejt (University of Oxford)
• Hongyang Qu (University of Sheffield)
• Jorge Julvez (University of Zaragoza)
• Ernst Moritz Hahn (Chinese Academy of Sciences)
• Bjorn Wachter (University of Oxford)
• Lijun Zhang (Chinese Academy of Sciences)
• Peter Biro (Hungarian Academy of Sciences)
• Alessandro Abate (University of Oxford)
• Aleksandra Jovanovic (University of Oxford)
• Alice Miller (University of Glasgow)
• Gabriel Santos (University of Oxford)

Projects

• 1998 - ... the probabilistic model checker PRISM
  
• 2007 - 2009 UbiVal: Fundamental Approaches to Validation of Ubiquitous Computing Applications and Infrastructures
  EPSRC Research Grant EP/D077273/1
• 2006 - 2007 Predictive modeling of signalling pathways via probabilistic model checking with PRISM
  Funded by Microsoft Research Cambridge under the computational tools for advancing science call (MRL contract 2005-04)
• 2003 - 2006 Probabilistic Model Checking of Mobile Ad Hoc Network Protocols
  EPSRC Research Grant GR/S46727
• 2003 - 2006 A Future Of Reliable Wireless Ad hoc networks of Roaming Devices (FORWARD)
  Part of the Next Wave Technologies and Markets DTI sponsored programme
• 2000 - 2003 Verification of Quality of Service Properties in Timed Systems
  EPSRC Research Grant GR/N22960
• 1998 - 2001 Automatic Verification of Randomized Distributed Algorithms
  EPSRC Research Grant GR/M04617
• 1998 - 2001 Stochastic Modelling and Verification
  Collaboration with University of Edinburgh, University of Mannheim and University of Erlangen-Nurnberg and funded by the British Council/DAAD

Teaching

I am currently teaching the following courses:

• Algorithmic Foundations 2
• Algorithmics I

I am the head of honours and was previously level 3 year head between 2020–2015 and coordinated masters project between 2011–2015. I am a fellow of the Higher Education Academy.

Contact