14 - 17 May 2001, Rennes, France.

The essence of Messega Sequence Charts

Java and the Java Virtual Machine: Verifying and validating bytecode verification and execution

The modularity of the ASM definitions for Java, the JVM and the compilation scheme exhibit orthogonal language, machine and compiler components, which fit together and provide the basis for a stepwise and provably correct design--for--reuse. The above definition for the JVM is extended to a defensive JVM which can be used as Java independent platform for safely executing byte code. Separating the checking mechanism from the execution we obtain a model for the bytecode verifier which can be proved to be correct and complete. By extending the compiler to a certifying compiler we can prove our compiler to generate code which successfully passes the bytecode verifier. As last step this bytecode verifier is integrated into a loading machine which together with the executing ASM provides a full JVM model.

The construction makes use of new composition techniques for building complex ASMs. These abstract machines for Java, the JVM and the compiler have also been refined to executable machines, which have been validated through experimentation with ASMGofer (available at http://www.uni-ulm.de/~s_jschmi/AsmGofer).

A full documentation is in the book R. Staerk, J. Schmid, E. Boerger: Java and the Java Virtual Machine: Definition, Verification, Validation. Springer-Verlag (2001), see http://www.inf.ethz.ch/~jbook

Developing Embedded Systems - where are Foundations needed?

On the generalized dining philosophers problem.

In the early 80's, Lehman and Rabin showed that there exist no deterministic, symmetric and fully distributed solution to the problem of the dining philosophers, and they proposed two randomized solutions: one which guarrantees deadlock freedom with probability 1 and another one which guarrantees lockout freedom with probability 1.

In this talk, we consider a generalization of the dining philosophers problem where the number of philosophers can exceed the number of forks (although each philosopher can still only access two forks), and we study whether the randomized algorithms of Lehman and Rabin still work in this situation. We show that the answer is "No": in most cases, a malicious scheduler can induce a deadlock. We then show a randomized solution, still fully distributed and symmetric, which works for any number of philosophers and any kind of connection graph, and guarrantees lockout freedom with probability 1.

On model checking security properties of cryptographic protocols

Temporal logic with(out) limits

- [](hist out \prefix hist in) /\ (lim out = lim in)

- hist c \prefix hist d and lim c \prefix lim d

- T |= lim c \prefix lim d

Bounded model checking for the universal subset of TCTL

Modeling interactive computation: Turing machines or labeled transition systems?

We present *Persistent Turing Machines* (PTMs), whose computation is
a stream-based and persistent extension of Turing machine (TM)
computation. A PTM repeatedly receives an input token from the
environment, computes for a while, and then outputs the result; moreover,
its work tape is persistent, so it ``remembers'' its previous contents
upon commencing a new computation. We show that the class of PTMs is
isomorphic to *interactive transition systems*, a very general class
of effective LTSs. As a result, PTMs admit a much richer variety of
equivalence relations than do TMs; bisimulation, and *persistent
stream language* (PSL) equivalence are examples.

We also consider *amnesic* PTMs, where each new computation begins
with a blank work tape, and a corresponding notion of equivalence based on
*amnesic stream languages* (ASLs). It can be argued that amnesic
stream languages are representative of the classical view of
Turing-machine computation. We show that the class of ASLs is strictly
contained in the class of PSLs. Furthermore, the hierarchy of PTM
equivalence relations collapses for the subclass of amnesic PTMs. One may
consequently conclude that, in a stream-based setting, the extension of
the Turing-machine model with persistence is a nontrivial one. It results
in a natural model of sequential interactive computation, offering a
bridge between TM-based computational models and those based on LTSs, and
providing a formal foundation for reasoning about interactive computation.

Extensionality and intensionality in the Ambient Logic

First-order logic on traces

Abstract interpretation: an algebraic approach

A New Version of Action Semantics

Proof-Outlines for Threads in Java

Limits of optimal parallel flow analysis