**IFIP
WG 2.2 Meeting Bologna**

September 05-06, 2009

**Titles
and abstracts of talks**

(in chronological order)

**Speaker:
Frank de Boer
Title: On Deadlock Detection of Reentrant Multithreaded Programs
Abstract: **

Missing.

**Speaker:
Luis Caires
Title: On Session Types and Linear Logic
Abstract: **

**Speaker:
Jan Rutten
Title: Kleene Coalgebra
Abstract: **

We present an overview of four recent papers:

1. Marcello Bonsangue, Jan Rutten, Alexandra Silva.

Coalgebraic logic and synthesis of Mealy machines.

FoSSaCS 2008.

2. Marcello Bonsangue, Jan Rutten, Alexandra Silva.

A Kleene theorem for polynomial coalgebras.

FoSSaCS 2009.

3. Marcello Bonsangue, Jan Rutten, Alexandra Silva.

Algebras for Kripke polynomial coalgebras.

LICS 2009.

4. Filippo Bonchi, Marcello Bonsangue, Jan Rutten,

Alexandra Silva. Deriving syntax and axioms for

quantitative regular behaviours.

CONCUR 2009.

**Speaker:
Einar Broch Johnsen
Title: Runtime Evolution of Distributed Concurrent Objects
Abstract: **Many long-lived and distributed systems must remain available
yet evolve over time, due to, e.g., bugfixes, feature extensions, or changing
user requirements. To facilitate such changes, formal methods can help in
modeling and analyzing runtime software evolution. This paper presents an
executable object-oriented modeling language which supports runtime software
evolution. The language, based on Creol, targets distributed systems by active
objects, asynchronous method calls, and futures. A dynamic class construct
is proposed in this setting, providing an asynchronous and modular upgrade
mechanism. At runtime, class redefinitions gradually upgrade existing instances
of a class and of its subclasses. An upgrade may depend on previous upgrades
of other classes. For asynchronous runtime upgrades, the static picture may
differ from the actual runtime system. An operational semantics and a type
and effect system are given for the language. The type analysis of an upgrade
infers and collects dependencies on previous upgrades. These dependencies
are exploited as runtime constraints to ensure type safety.

**Speaker:
Davide Sangiorgi
Title: Termination in higher-order concurrent languages
Abstract: **

**Speaker:
Barbara Koenig
Title: Applying the Graph Minor Theorem to the Verification of Graph
Transformation Systems
Abstract: **

We show how to view certain subclasses of (single-pushout)
graph transformation systems as well-structured transition systems, which
leads to decidability of the covering problem via a backward analysis. As
the well-quasi order required for a well-structured transition system we use
the graph minor ordering. We sketch an explicit construction of the backward
step and apply our theory in order to show the correctness of a leader election
protocol.

**Speaker:
Javier Esparza
Title: Newtonian Program Analysis
Abstract: **

In this talk I'll look at a sequential program as a system of equations of the form

X_1 = f_1(X_1, ..., X_n)

...

X_n = f_n(X_1, ..., X_n)

where the f_i's are polynomials, and sum and product correspond to choice
and sequential composition. (If you're familiar with process algebras, this
should ring a bell.) I'll argue that static program analysis is the art of
solving these equations over different interpretations,

depending on the information one is interested in.

After 40 years of research on static analysis we have not produced much theory on *generic* methods for solving these equations, i.e., on methods that work for *any* interpretation. The ones around are based on Knaster-Tarski's and Kleene's theorems. Unfortunately, these methods rarely terminate for infinite domains, and in metric interpretations their convergence is often hopelessly slow. Can't we do better?

I'll show that Newton's method, well-known from numerical mathematics, can be generalized to (almost) arbitrary interpretations, and that this generalization provides a unified view of many results of language theory, as well as a bridge between qualitative and quantitative program analysis.

(Joint work with Stefan Kiefer and Michael Luttenberger)

**Speaker:
Ugo Montanari
Title: Models for Open Transactions
Abstract: **

Loosely coupled interactions permeate modern distributed systems, where autonomous applications need to collaborate by dynamical assembly. We can single out three different phases occurring in every collaboration: 1) negotiation of some sort of contracts, mediating the needs of prospective participants; 2) acceptance or rejection of the contract; 3) contract-guarantee execution. The above scheme, called NCE for short (Negotiation, Commit, Execution), covers a wide range of situations, ranging from sessions and transactions to proof-carrying code. In the talk we concentrate on the notion of open transaction and on Zero-Safe Nets, a model developed by Bruni and Montanari for modelling long transactions. We extend the latter to cover the three-phase process above.

(Joint work with Roberto Bruni)

**Speaker:
Rocco De Nicola
Title: Rate-based Transition Systems for Stochastic Process Calculi
Abstract: **

A variant of Rate Transition Systems (RTS) is introduced and used as the basic model for defining stochastic behaviour of processes and for associating Continuous Time Markov Chains to process terms. The transition relation used in our variant associates to each process, for each action, the set of possible futures paired with a measure indicating their rates.We show how RTS can be used for providing the operational semantics of stochastic extensions of classical formalisms, namely CSP and CCS. We also show that our semantics for stochastic CCS guarantees associativity of parallel composition. Similarly, in contrast with the original definition by Priami, we argue that a similar approach for defining the semantics of stochastic pi-calculus guarantees associativity of parallel composition.

(Joint work with Diego Latella, Michele Loreti and Mieke Massink)

**Speaker:
Joost-Pieter Katoen
Title: Abstraction of Probabilistic Systems: From Theory to Practice
Abstract: **

**Speaker:
Marjan Sirjani
Title: Actors Performing: Domain Specific Modeling and Analysis
Abstract: **

The Reactive Object Language, Rebeca, is an imperative interpretation of actors
which is designed as an analyzable modeling language for real-world applications.
It is supported by model checking tools and compositional verification approaches.
Reduction techniques including slicing, partial order and symmetry detection
are developed based on the computational model of Rebeca.

Rebeca has a simple kernel and is extended specifically for the domain of
applications. In this talk, we present the computational model of Rebeca,
its analysis techniques, and extensions for various domains.

**Speaker:
Uwe Nestmann
Title: Use Process Calculi for Fault-Tolerant Distributed Algorithms?
Abstract: **

More precisely, we sketch Milner's scheduler example as known from his textbook and examine the involved proof strategy. It is essentially based on a concise notation to capture all reachable states in a way that makes it possible to succinctly describe and analyze invariants. The actual proofs then involve so-called "bisimulation up-to" techniques.

Following this strategy, we show that it indeed scales up to the chosen case
study: a distributed consensus algorithm due to Chandra and Toueg in the context
of the failure detector S. Apart from the fact that this algorithm requires
non-trivial analysis work, we conclude that using process calculi this way
provides us with a useful tool to formally connect an invariant-style state-based
reasoning to the underlying algorithm code (formally spelled out within the
process calculus, as opposed to informal pseduo code).

**Speaker:
Igor Walukiewicz
Title: Weak Alternating Timed Automata
Abstract: **

**Speaker:
Radu Grosu
Title: Finite Automata as Time-Invariant Linear Systems: Observability, Reachability
and More
Abstract: **

We show that regarding finite automata (FA) as discrete, time-invariant linear systems over semimodules, allows to: (1) Express FA minimization and FA determinization as particular observability and reachability transformations of FA, respectively; (2) Express FA pumping as a property of the FA's reachability matrix; (3) Derive canonical forms for FAs. These results are to our knowledge new, and they may support a fresh look into hybrid automata properties, such as minimality. Moreover, they may allow to derive generalized notions of characteristic polynomials and associated eigenvalues, in the context of FA.

Published in Proc. of HSCC'09, the 12th International Conference on Hybrid

Systems: Computation and Control, San Francisco, USA, April, 2009, pp. 194-208,

Springer, LNCS 5469.

*This work was supported by the NSF Faculty Early Career Development Award

CCR01-33583 and the NSF CCF05-23863 Award.

**Speaker:
Anders Ravn
Title: Rigorous abstraction from continuous control to automata
Abstract: **