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 Glenn Bruns, Bell Labs / Lucent Technologies Dimitar Guelev, Bulgarian Academy of Sciences Steve Kremer, École Normale Supérieure de Cachan, France Stephanie Delaune, École Normale Supérieure de Cachan, France Stefano Cattani, University of Birmingham Pierre Yves Schobbens, University of Namur, Belgium Alessio Lomuscio, University College, London, UK Franck Cassez, Nantes, France Michael Huth, Imperial College, London, UK Dieter Ehrich, Braunschweig, Germany

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) (2009) Tien Tuan Anh Dinh (Security of peer-to-peer systems) (2009)

Research coordination Programme/organising committee memberships EPSRC College member, 2006-2009. Programme Committee member, ICALP (Track C), 2007. Dagstuhl Workshop organiser, Formal Protocol Verification Applied, 2007 Programme Committee member, 19th IEEE Computer Security Foundations Workshop (CSFW), 2006. Programme Committee member, 4th ACM Workshop on Formal Methods in Security Engineering (FMSE), 2006. Programme Committee member, Workshop on Trustworthy Elections (WOTE), 2006 Co-chair of the 8th International Conference on Feature Interactions in Telecommunications and Software Systems. Programme Committee member, 4th ACM Workshop on Formal Methods in Security Engineering, 2006. Programme Commitee member, Temporal Representation and Reasoning (TIME), 2005. Programme Committee member, 2nd, 3rd International Colloquium on Theoretical Aspects of Computing, 2005, 2006. Programme Committee member, Workshop on Foundations of Computer Security (FCS), 2005. Programme Committee member, 2nd, 3rd, 4th Model Checking and Artificial Intelligence (MoChArt), 2002, 2005, 2006. Co-organiser of Modelling and Verifying Parallel Processes (MOVEP), 2004 Dagstuhl Workshop organiser: Objects, agents and aspects, 16-21 February 2003. Proceedings Summer School on Modelling and Verifying Parallel Processes, 2000, 2002. Fifth, Sixth, Seventh International Workshop on Feature Interactions in Telecommunications and Software Systems, 1998, 2002, 2003. LICS'98 Workshop on Probabilistic Methods in Verification. Practical Reasoning and Rationality 1998, Practical Reasoning and Rationality 1997.

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) 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) 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.