Keywords: verification, semantics, distributed systems, message passing, value passing, lambda calculus, pi calculus

Start Date: 1 January 95 / Duration: 36 months

[ participants / contact]

Objectivies and Approach

The goal is to develop robust verification tools for distributed systems based on a solid theoretical understanding of their semantics. This requires both fundamental research into semantics for processes as well as the development of software tools using modern high-level languages such as Standard ML, and high-level interfaces to x-windows.

Progress and Results

In previous work, a symbolic version of the standard bisimularity checking algorithm was developed for finite symbolic graphs. However, with this formalism there were difficulties to ensure that the symbolic graphs generated from the expressions of a value-passing process language are finite. The symbolic graphs have now been generalised to include information about assignments. The resulting formalism is much more powerful for capturing the intentional behaviour of value-passing processes, and the symbolic version of the bisimulation checking algorithm has been extended to this more general formalism.

Information Dissemination Activities and/or Exploitation

The above mentioned results have been presented at the international conference CONCUR'96, which was held in Pisa in August 1996.


University of Sussex
Falmer Street
Brighton, UK

EU Partners

University of Sussex, UK
Laboratoire d'Informatique de l'EcoleNormale Superieure, F

Non-EU Partners

Institute of Software, Chinese Academy of Sciences, CHI


Prof. Matthew Hennessy
Tel: +44 1273 678 195
Fax: +44 1273 671 320

INCO synopses home page INCO cooperation index INCO keyword index
INCO acronym index INCO number index INCO Working Groups index
synopses home page all keywords index all acronyms index all numbers index

SYMSEM - KIT119, May 1997

please address enquiries to the ESPRIT Information Desk

html version of synopsis by Nick Cook