Research Interests

• model checking
• probabilistic verification
• verification of real-time and hybrid systems
• concurrency theory
• probabilistic and real-time process algebras
• performance modelling

Publications

See an online list of publications.

Program committees

• Fourth International Conference on the Quantitative Evaluation of Systems (QEST'07)
• Fifth International Conference on Computational Methods in Systems Biology (CMSB'07)
• Third International Conference on the Quantitative Evaluation of Systems (QEST'06)
• Second International Workshop on Practical Applications of Stochastic Modelling (PASM'05)
• Second International Conference on the Quantitative Evaluation of Systems (QEST'05)
• First International Workshop on Practical Applications of Stochastic Modelling (PASM'04)

Collaborators

• Marta Kwiatkowska (University of Oxford)
• Dave Parker (University of Oxford)
• 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)
• Conrado Daws (University of Nijmegen)
• Antonio Pacheco (Instituto Superior Tecnico Lisboa)
• Markus Siegle (Universitat der Bundeswehr Munchen)
• Holger Hermanns (Saarland University)
• Sylvain Peyronnet (EPITA Research and Development Laboratory)
• 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)

Projects

• UbiVal: Fundamental Approaches to Validation of Ubiquitous Computing Applications and Infrastructures
  2007 -
  EPSRC Research Grant EP/D077273/1
  
  
• PRISM
  September 1998 -

  A state of the art probabilistic symbolic model checker using Binary Decision Diagrams and Multi-Terminal Binary Decision Diagrams.

• Predictive modeling of signalling pathways via probabilistic model checking with PRISM
  2006 - 2007
  Funded by Microsoft Research Cambridge under the Computational tools for advancing science call for papers (MRL contract 2005-04)

  Understanding biological processes, and especially how the cells interact and make decisions, is an essential step towards predictive biology and personalized medicine. Experimental biology is contributing key data towards this goal, but suffers from inherent inaccuracy of observations compounded by the natural variability of biological systems. Systems biology seeks sound scientific understanding of biological processes through a cycle of experimental research and hypothesis generation formed with the help of computational tools for in silico modelling. This proposal contributes to the predictive biology effort by adapting process calculi and the probabilistic model checking technology, and specifically the leading probabilistic model checker PRISM developed at the University of Birmingham, to the study of biological processes. This complements the traditional differential equations (ODE) modelling approaches and offers new ways to affirm or disprove scientific hypotheses.

• Probabilistic Model Checking of Mobile Ad Hoc Network Protocols
  November 2003 - October 2006
  EPSRC Research Grant GR/S46727

  This project aims to investigate the foundations of modelling and analysis of mobile ad hoc network protocols, with the view to develop automated design validation methods capable of performance prediction and correctness assurance. Performance prediction, an essential factor when evaluating ad hoc network designs due to mobility, inherent delays in the underlying transmission mechanism and potential loss of interconnectivity, will be achieved through the novel probabilistic model checking techniques developed at Birmingham with EPSRC support. The functional correctness of the designs will be established by invoking verification via model checking, an automatic method that addresses the deficiencies of simulation by exploring all the possible executions of designs.

• A Future Of Reliable Wireless Ad hoc networks of Roaming Devices (FORWARD)
  2003 - 2006

  Part of the Next Wave Technologies and Markets DTI sponsored programme.

• Verification of Quality of Service Properties in Timed Systems
  May 2000 - July 2003
  EPSRC Research Grant GR/N22960

  This project aims to address the foundations of the verification of quality of service properties of real-time systems. The work will concentrate on the development of a suitable model, high-level specification languages, industrially-relevant case studies and efficient model checking algorithms. The approach advocated here should not be viewed as an alternative to methods such as simulation, testing and verification via theorem proving, but rather as a complementary technique.

• Automatic Verification of Randomized Distributed Algorithms
  September 1998 - September 2001
  EPSRC Research Grant GR/M04617

  This project is concerned with extending the model checking techniques to the case of randomized distributed algorithms. These are algorithms which are designed to run on hardware consisting of many interconnected processors (and often geographically `distributed', as in the case of a network of processors), and which use randomization, that is, make choices at random, using electronic coin flipping. It turns out that randomized algorithms are much faster than their deterministic counter- parts, but verifying their correctness against the specification is much more involved because of the need for sophisticated probabilistic analysis. Moreover, a model checker may be unable to output `yes' or `no', but instead only the probability of the specification being satisfied.

• Stochastic Modelling and Verification
  July 1998 - July 2001
  Collaboration with University of Edinburgh, University of Mannheim and University of Erlangen-Nurnberg
  Funded by the British Council/DAAD

  This research is concerned with stochastic modelling and verification of computer systems such as distributed systems and communication protocols. The project will focus on advancing the semantic foundations of stochastic process algebras. We will concentrate on: formulating a logic-based specification language for Markovian process algebras, efficient model checking methods for systems with probability and time, and developing the semantic foundations for stochastic process algebras with general distributions

CV

My CV is available from here.