25 - 29 September 2000, Oldenburg, Germany.

Reducing Model Checking from Multi-Valued CTL* to CTL*

A Coinductive Calculus of Component Connectors

Here we shall present a relational model for (a fragment of) Reo,
constructed in terms of streams, that is, infinite sequences.
The set of all streams is a final coalgebra and therewith
comes equipped with coinduction definition and proof principles.
One of the crucial features of Reo is the fact that through
subtle timing, various coordination patters can be established.
This will be captured in our model by considering not only
data streams but also so-called time streams. Thus we shall have
a double benefit of our coinductive machinery:
it applies both to data streams and to time streams.

Validating Model Translations

Specification of Transacted Memory in Smart Cards Using Java and JML

Programs running on a smart card can be interrupted at any moment by a sudden loss of power, namely when someone removes the smart card from the card reader. Therefore the miniature operating system on the smart card has to provide support for "transactions", updates of the persistent memory of the smart card that are atomic, in the sense that any partial updates that are interrupted by a loss of power will be undone when the card start up again.

The central issue in the specification of the transacted memory is
how to model the interruption of a program by a loss of power. This
also affects the Hoare logic to be used to reason about programs
running on the smart card.

Abstract A+ Algorithm and Applications (Recent Work on Timed Systems)

Exact Dependence Analysis in Parallel Programs

Another Look at tau and Time: Verification on Timed Algebra

Probabilistic Automata and Compositionality

This shows that the natural extension of trace inclusion leads to a branching relation rather than to a linear relation. Although alternative linear relations that extend trace inclusion do exist, the real problem is to find meaningful linear relations, which is currently still open.

The contents of this talk include results that are joint work with Nancy
Lynch and Frits Vaandrager.

Toward a Mobile TLA

A Sound and Complete Hoare logic for a Sequential Subset of Java

M3: Mobility Types for Mobile Processes in Mobile Ambients

Components

On the Expressive Power of Temporal Constraint Programming Language

Regular Extrapolation

Reflection on Modelling Names and Binders (Induction, Recursion and Bialgebras on Terms up to alpha-equivalence)