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
Parameterized Verification via Monotonic Abstraction
Parosh Aziz Abdulla (Uppsala University, Sweden)
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.
Concurrent Bugs: How to Eliminate Them or Render Them Harmless
Shmuel Ur (IBM Haifa Research Laboratories, Israel)
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
Metric Embeddings and Algorithms
Jiří Matoušek (Charles University, Czech Republic)
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.
Mogens Nielsen (BRICS, Aarhus, Denmark)
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
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
Programming Models for Grid Applications and Systems
Thilo Kielmann (Vrije Universiteit, Netherlands)
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: