Details of Grant 

EPSRC Reference:	GR/M04617/01
Title:	AUTOMATIC VERIFICATION OF RANDOMIZED DISTRIBUTED ALGORITHMS
Principal Investigator:	Kwiatkowska, Professor MZ
Other Investigators:	Ryan, Professor M
Researcher Co-Investigators:
Project Partners:
Department:	School of Computer Science
Organisation:	University of Birmingham
Scheme:	Standard Research (Pre-FEC)
Starts:	01 September 1998	Ends:	31 August 2001	Value (£):	142,550
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:
Summary on Grant Application Form
Distributed algorithms are those which run on hardware consisting of many interconnected processors. Randomised distributed algorithms further employ a random element, such as a random number generator or electronic coin flipping, are often simpler and more efficient than their deterministic counterparts. Randomised distributed algorithms are useful in applications such as message routing and co-ordinating distributed computer networks. However, they are often hard to reason about: the probabilistic analysis becomes complex, and the algorithms are often subtle.We intend to develop methods to automate the verification process of randomised algorithms, all or in part, by extending conventional model checking techniques. We will develop the theoretical foundations by identifying appropriate specification and description languages, models, verification algorithms and efficient data structures, and work with the developers of verification tools to develop prototype systems. These prototypes should support the validation of a range of classes of properties, from computation of time bounds to probabilistic temporal properties. Examples and case studies will be used to evaluate the success of our methods; these will vary from the relatively simple Byzantine agreement, to more complex randomised protocols. We will build upon our existing collaboration with the group at CMU (USA), and initiate new collaborations.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.bham.ac.uk