**IFIP
WG 2.2 Meeting Paris**

September 21-23, 2011

**Titles
and abstracts of talks**

(in chronological order)

**Speaker:
Igor Walukiewicz
Title: Krivine machines and higher order schemes
Abstract: **

We discuss a new approach to analysing higher-order recursive schemes. Many results in the literature use automata models generalising pushdown automata, most notably higher-order pushdown automata with collapse (CPDA). Instead, we propose to use the Krivine machine model. Compared to CPDA, this model is closer to lambda-calculus, and incorporates nicely many invariants of computations, as for example the typing information. The usefulness of the proposed approach is demonstrated with new proofs of two central results in the field: the decidability of the local and global model checking problems for higher-order schemes with respect to the mu-calculus.

**Speaker:
Christel Baier
Title: On Operational Semantics of Message Sequence Graphs
Abstract: **

**Speaker:
Kohei Honda
Title: Sessions, Types and Logics
Abstract: **

**Speaker:
Gilles Barthe
Title:Computer-Aided Security Proofs for the Working Cryptographer
Abstract: **

**Speaker:
Einar Broch-Johnsen
Title: Deployment Components with Parametric Resources
Abstract missing **

**Speaker:
Andrzej Tarlecki
Title: Compositional Property-oriented Semantics for Structured
Specifications. Another Old Story (with a Few New Twists)
Abstract: **

We discuss property-oriented semantics of specifications built using
some collection of specification-building operations. Working in an
arbitrary institution, we consider the structured specifications built
from flat specifications using union, translation and hiding. We then
have the standard compositional proof system, which determines the
standard property-oriented semantics assigning a theory to each
structured specification. It is not complete (unless the underlying
logic has interpolation and enjoys some other technical properties)
but otherwise it is "as good as can be expected". In particular, it is
sound, monotone (and hence compositional) and closed complete. The
last property means that the semantics (and the corresponding proof
system) allows us to deduce all true consequences for specifications
built by applying any specification-building operation to argument
specifications, assuming that there is no discrepancy between the
classes of models of the argument specifications and the classes of
models of their respective property-oriented meanings. This was
believed to ensure that the semantics is "as strong as possible"
without loosing soundness and compositionality. We question this claim
and show that it holds assuming in addition that the semantics
considered are theory-oriented, i.e., the sets of properties assigned
to specifications are closed under consequence, as well as
non-absent-minded, i.e., no axioms from flat specifications are
omitted as properties. We sketch examples to show that neither of
these requirements may be dropped. We generalise this to the context
of entailment systems, and show similar results and counterexamples.

**Speaker:
Frank de Boer
Title: Run-time Assertion Checking of Communication Histories in Java using Attribute Grammars
Abstract: **

**Speaker:
Marco Pistore
Title: Composition (and Adapatation) of Service Based Applications
Abstract: **

In the talk, we discuss the problem of service composition with
digressions on service adaptation, two of the most challenging problems
of the Service Oriented Computing paradigm. After an overview of these
problems, we describe ASTRO, a framework for service composition and
adaptation that has been developed in Trento during the last years, and
that has been exploited both in research and in industrial projects. In
particular, we show that, while service composition and service
adaptation are in general intractable problems, in practical contexts
they are used under specific conditions that make them tractable;
moreover, as ASTRO witnesses, in these contexts formal methods provide
practical and effective solutions to service composition and adaptation.

**Speaker:
Uwe Nestmann
Title: Synchronous and Asynchronous Interaction in Distributed Systems
Abstract: **

**Speaker:
Peter Mosses
Title: PLanCompS: Programming Language Components and Specifications
Abstract: **

PLanCompS [www.plancomps.org] is a 4-year joint research project, based
at Swansea, Royal Holloway and City, starting in September 2011. It is
funded by EPSRC grant EP/I032495/1 and related grants.

**Speaker:
Ugo Montanari
Title: Component-Based Network Models
Abstract: **

(Joint work with Roberto Bruni, Pisa & Hernan Melgratti, Buenos Aires. Work supported by FET-IST EU project ASCENS)

**Speaker:
Patricia Bouyer
Title: Quantitative Models for Verification, a timed-automata-based perspective
Abstract: **

**Speaker:
Wojciech Penczek
Title:
A Practical Approach to Parametric Model Checking
Abstract: **

**Speaker:
Leslie Lamport
Title: What Will it Take to Get You to Teach With PlusCal?
Abstract: **

PlusCal is an algorithm language based on TLA+. A PlusCal algorithm is automatically translated to a TLA+ specification that can be checked with the TLC model checker or reasoned about formally. PlusCal makes pseudo-code obsolete. It is the ideal language for teaching sequential, concurrent, and distributed algorithms.

**Speaker:
Ernst-Rüdiger Olderog
Title: An Abstract Model for Proving Safety of Multi-Lane Traffic Manoeuvres
Abstract: **

We present an approach to prove safety (collision freedom)
of multi-lane motorway traffic with lane-change manoeuvres.
This is ultimately a hybrid verification problem due to
the continuous dynamics of the cars.
We abstract from the dynamics by introducing a new
spatial interval logic based on the view of each car.

To guarantee safety, we present
two variants of a lane-change controller, one
with perfect knowledge of the safety envelopes of neighbouring
cars and one which takes only the size of the
neighbouring cars into account.
Thereby we assume that each car
can communicate with its neighbouring cars and
is equipped with suitable sensors.
The guards and state invariants of the controllers
are described in the new logic.

Based on these controllers we provide a local safety proof
for unboundedly many cars
by showing that at any moment the reserved space of each car
is disjoint from the reserved space of any other car.

(joint work with Martin Hilscher, Sven Linker and Anders P. Ravn)

**Speaker:
Catuscia Palamidessi
Title: Differential Privacy and Relation with Quantitative Information Flow
Abstract: **

Differential privacy is a notion of privacy that has become very
popular in the database community. Roughly, the idea is that a
randomized query mechanism provides sufficient privacy protection if the
ratio between the probabilities that two adjacent datasets give the
same answer is bound by $e^\epsilon$. In the field of information flow
there is a similar concern for controlling information leakage, i.e.
limiting the possibility of inferring the secret information from the
observables. In recent years, researchers have proposed to quantify the
leakage in terms of R\'enyi min mutual information, a concept strictly
related to the Bayes risk.
In this talk, we show how to model the query system in terms of an
information-theoretic channel, and we compare the notion of differential
privacy with that of mutual information. We show that differential
privacy implies a bound on the mutual information, but not vice-versa.
Furthermore, we show that our bound is tight.
Then, we consider the utility of the randomization mechanism, which
represents how close the randomized answers are, in average, to the real
ones. We show that the notion of differential privacy implies a bound
on utility, also tight, and we propose a method that under certain
conditions builds an optimal randomization mechanism, i.e. a mechanism
which provides the best utility while guaranteeing
$\epsilon$-differential privacy.

**Speaker:
Marcelo Frias
Title: Automated Scope Bounded Code Analysis: State of the Art
Abstract missing **