Several talks by distinguished researchers from the different areas of interest of the workshop will be a part of the programme. The invited speakers and the titles of their talks will be published shortly.

Several classes of programs can be modeled as infinite transition systems where the transition relation is monotonic with respect to a certain natural ordering on the set of states. Examples include Petri nets, lossy channel systems, timed networks, multiset rewriting systems, broadcast protocols, etc. On the other hand, there are also classes of programs whose behaviours do not satisfy the monotonicity condition. In this talk, we present the notion of "monotonic abstractions" which transforms a non-monotonic transition system into a monotonic one through an over-approximation. This enables us to adapt methods developed for the above models for verifying non-monotonic systems. We illustrate the method through applications to verification of parameterized systems, and to shape analysis of programs manipulating dynamic data structures.

Concurrency is everywhere. Moore law no longer apply is it once did and if one wants to gain performance the application has to be concurrent. Creating concurrent program is so hazard prone that it is a common belief that the current programming methodology does not scale. This talk will first describe why getting concurrent programs to work correctly is so difficult, with focus on testing and debugging issues. Then a short survey of relevant technologies will be given. Lastly a few promising research directions in the area of testing, debugging and healing concurrent bugs will be detailed.
Slides from the presentation

We consider approximate embeddings of finite metric spaces into Euclidean spaces (and possibly other normed spaces). These were first studied in mathematical contexts, but more recently they have become a very powerful tool for approximation algorithms, clustering, data simplification, database querying, and other algorithmic applications. Some of the results and methods will be illustrated on examples and case studies.

The vision of Ubiquitous Computing, i.e. a scenario of computing of the future consisting of billions of mobile devices communicating and sharing a vast amount of resources and information, raises many new challenges with respect to security-related issues. This is the main motivation for some recent research in Computational Trust as an alternative to traditional security mechanisms, the idea being that applications make decisions based on a suitable computational notion of trust. This talk will survey some of the main systems and models from Computational Trust (including credential based as well as reputation based approaches). Based on this, we argue for the need of research into formal frameworks for comparing the quality of different trust-based systems, and we illustrate some preliminary ideas in this direction.

Writing grid applications is hard. By now, there is a large variety of grid middleware, each providing its own set of application interfaces. Only little analysis has been done about the requirements of applications, and how they could be translated to a grid programming model.
In this talk, we analyze both functional and non-functional application programming requirements for grids and present the programming environments (co-)developed within our group: Ibis, the JavaGAT, and SAGA.
Further info available at: www.cs.vu.nl/ibis, saga.cct.lsu.edu

•