Mark Ryan - Research

interests · activities · projects · PhD students

Research interests

My work broadly concerns reasoning about computer systems, in order to verify their properties.
In particular, I work on logic-based specification and verification of systems and programs.


Research topics

  • Specifying and verifying systems
    • Designing languages and tools to model systems
    • Model checking
    • Systems which are composed of features, and analysing feature interactions (more...)
  • Reasoning about computer security
    • Verifying protocols, such as
      • electronic voting protocols (more...)
    • Verifying access control systems (more...)
  • Logic
    • All kinds of logic, such as first-order logic, temporal logic and modal logic
  • Applications of logic in artificial intelligence
    • Belief revision
    • Non-monotonic reasoning

Recent and current collaborators

PhD Students

Name Topic (Exp.) Compl. Date
Sofia Guerra Specification of reactive systems using defaults 1999
Alessio Lomuscio Logics for multi-agent systems 1999
Malte Plath Feature integration 2000
Nikos Gorogiannis Computing Minimal Changes of Models of Systems 2003
Aidan Harding Symbolic synthesis of strategies for infinite games 2004
Hannah Harris Feature integration and its logical properties 2005
Nan Zhang
 Analysis of access control systems
 2006
Andrew Brown
 (Verifying untrusted software)
 (2008)
Anongporn Salaiwarakul
 (Verifying biometric protocols)
 (2008)
Hasan Qunoo
 (Verifying access control policies via model checking)
 (2010)
Ben Smyth
 (Validation of security in ubiquitous computing applications) (2010)
Tien Tuan Anh Dinh
 (Security of peer-to-peer systems)
 (2009)

Research coordination

Programme/organising committee memberships

Externally funded projects

  • Source of Funds: EPSRC (UK)
    Title of Project: Verifying anonymity and privacy properties of security protocols
    Start Date: 1 April 2007
    Duration: 18 months
    Total Value: £134,762
    Grant Holders:  M. Ryan

  • Source of Funds: EPSRC (UK)
    Title of Project: Verifying Properties in Electronic Voting Protocols
    Start Date: 1 September 2006
    Duration: 4 months
    Total Value: £35,000
    Grant Holders:  M. Ryan

  • Source of Funds: IBM Faculty Award
    Title of Project: Policy languages for access control
    Start Date: Sept 2006
    Duration: 18 months
    Total Value: £20,000
    Grant Holders: M. Ryan

  • Source of Funds: EPSRC (UK)
    Title of Project:  UbiVal: Fundamental approaches to validation of ubiquitous computing applications and infrastructures
    Start Date: October 2006
    Duration: 4 years
    Total Value: £567,536
    Grant Holders:  M. Z. Kwiatkowska, M. D. Ryan, D. Ghica

  • Source of Funds: EPSRC (UK) EP/D000122
    Title of Project:  International Conference on Feature Interactions.
    Start Date:  March 2005
    Duration: 5 months
    Total Value:  £8,050
    Grant Holders:  S. Reiff-Marganiec, M. Ryan

  • Source of Funds: EPSRC (UK) GR/R02214
    Title of Project: The feature construct in programming and specification languages.
    Start Date: 1 August 2001
    Duration: 36 months
    Total Value: 183,384 pounds.
    Grant Holders: Mark Ryan and Marta Kwiatkowska.

  • Source of Funds: EPSRC (UK)
    Title of Project: Automatic Verification of Randomized Distributed Algorithms.
    Start Date: 1 September 1998
    Duration: 36 months
    Total Value: 142,550 pounds.
    Grant Holders: Marta Kwiatkowska and Mark Ryan.

  • Source of Funds: EPSRC (UK)
    Title of Project: Formal Analysis of Randomized Distributed Algorithms: Visiting Fellowship for R Segala.
    Start Date: 1 September 1998
    Duration: 36 months
    Total Value: 8,820 pounds.
    Grant Holders: Marta Kwiatkowska and Mark Ryan.

  • Source of Funds: ESPRIT (European Union)
    Title of Project: FIREworks - Feature Integration in Requirements Engineering.
    Start Date: 1 May April 1997
    Duration: 42 months
    Total Value: 172 800 Euro.
    Grant Holders: M. D. Ryan (co-ordinator), and others.

  • Source of Funds: ESPRIT (European Union)
    Title of Project: ASPIRE - Advanced modeling and SPecification of distributed InfoRmation systEms.
    Start Date: February 1997
    Duration: 36 months
    Total Value: 165 000 Euro (total), c. 10 000 Euro (Birmingham).
    Grant Holders: H.-D. Ehrich (coordinator), M. D. Ryan (Birmingham), and others.

  • Source of Funds: British Telecom
    Title of Project: Feature Specification Languages.
    Start Date: January 1997
    Duration: 36 months
    Total Value: 49 671 pounds.
    Grant Holders: M. D. Ryan.

  • Source of Funds: The Nuffield Foundation
    Title of Project: Default Reasoning Applied to Specification and Design of Computer Systems.
    Start Date: January 1996
    Duration: 24 months
    Total Value: 2 800 pounds.
    Grant Holders: M. D. Ryan.

  • Source of Funds: ESPRIT (European Union)
    Title of Project: ModelAge - Formal MODELs of AGEnts.
    Start Date: May 1994
    Duration: 36 months
    Total Value: c. 100 000 Euro (total), c. 10 000 Euro (Birmingham).
    Grant Holders: P.-Y. Schobbens (co-ordinator), M. D. Ryan (Birmingham site), and others.

  • Source of Funds: British Council / JNICT
    Title of Project: Defaults in Specifications.
    Start Date: February 1995.
    Duration: 12 months
    Total Value: 2000 pounds.
    Grant Holders: A. Sernadas and M. D. Ryan.