IFIP WG 2.2 Meeting Nancy

September 17-19, 2007

Titles and abstracts for talks

(in chronological order)

Speaker: Davide Sangiorgi
Title: Some remarks on equality and bisimulation in higher-order languages
I discuss some of the approaches to defining equality between terms of (sequential) higher-order languages (eg, the lambda-calculus). In particular I discuss bisimulation, recalling the "standard" definition of bisimulation in lambda-calculus and proposing some modifications to it.

Speaker: Jan Rutten
Title: Coinduction: basics, examples, variations
We present the basics of coinduction in terms of (final) coalgebra; illustrate it by means of some examples; and conclude by showing some recent extensions and variations.

Speaker: Barbara Koenig
Title: Verification of Graph Transformation Systems
In this talk I give an overview of existing verification methods for graph transformation systems. Graph transformation is an expressive modelling formalism that allows to specify systems with an infinite state space, with dynamic creation and deletionof objects, with mobility and variable topology. These are desirable features which are shared by related formalisms such as calculi for mobility, bigraphs or evolving heap structures. However, they present a considerable challenge for state-of-the-art verification techniques.

The talk is structured as follows: first I will describe methods for finite-state systems (using model-checking tools, isomorphism checking and unfoldings), then I will talk about infinite-state systems (shape analysis, abstract graph transformation, approximated unfoldings). The
talk concludes with some considerations about logics.

Speaker: Luke Ong
Title: Verification of Higher Order Computation: a Semantic Approach
We present a systematic approach to the foundations of verifying higher-order computation using semantic methods. We consider higher-order pushdown automata and higher-order recursion schemes (and related families) as generators of possibly infinite ranked trees and graphs, and survey recent progress along two main directions:

1. Relationship between the families of generators in terms of their

2. Algorithmic properties of infinite structures that are thus generated.

Speaker: Peter D. Mosses
Title: BFLDL: Formal Language Description Library
We solicit WG 2.2 support for a proposed initiative to create a digital library of (formal) semantic descriptions of programming languages. With proper quality control and indexing, the library should solve the current problems with locating and accessing published semantic descriptions. Scanning to pdf would also ensure the preservation of descriptions from the early years - many of which were highly significant, and of intrinsic interesregarding the employed semantic description techniques, but now mostly out of print.

To support future semantic description of programming languages, the digital library could also include an evolving repository of reusable components in modular description frameworks such as Monadic Semantics, Modular SOS and Action Semantics.

WG 2.2 Members and Observers who have access to (printed or electronic) copies of significant semantic descriptions are requested to send the relevant publication data to


at their earliest convenience. It is anticipated that an initial version of the library will be available by summer 2008.

Speaker: Joost-Pieter Katoen
Title: Model Checking Probabilistic Systems
Model checking of random phenomena enjoys a rapid increase of interest
from different communities. Various software tools support the verification of Markov chains or variants thereof that exhibit nondeterminism. Applications range from randomised distributed algorithms, planning and AI, and security to biological process modeling and quantum computing. Verification engines have been integrated in existing tool chains for Petri nets, Statemate, and are used for a probabilistic extension of Promela, the input language of SPIN, one of the most widely used model checkers.

This talk reviews the foundations of this technique and discusses some of the recent advances such as algorithms for counterexample generation.

Speaker: Herbert Wiklicky
Title: Abstract Interpretation for Worst and Average Case Analysis

(joint work with Alessandra Di Pierro Universita di Verona)

Abstract: This presentation focused on comparing the theoretical foundations underlying
a coherent framework for qualitative and quantitative approaches in static program analysis. Central to such a unifying point of view are two closely related notions of ``approximation'' which formalise the concepts of ``correctness'' and ``closeness'' in different ways. This leads on the one hand to the framework of classical Abstract Interpretation (AI) based on
so-called Galois Connections - introduced by Cousot and Cousot in the 1970s - and on the other to Probabilistic Abstract Interpretation (PAI) based on the so-called Moore-Penrose Pseudo-Inverse - introduced by the authors. As an example, we discussed the concept of probabilistic bisimulation (introduced by Larsen and Skou) in the context of Probabilistic Abstract Interpretation, how to introduce an approximative version of this notion, as well as possible applications in the area of computer security.

Speaker: Uwe Nestmann
Title: Formal Methods (aka: Concurrency Theory) for Distributed Algorithms
The formal verification of distributed algorithms, in particular fault-tolerant ones, still represents a rather non-trivial challenge. The field of Concurrency Theory offers a range of methods and techniques to formally specify and possibly verify concurrent and distributed systems. In this talk, we focus on the use of process calculi on this matter. The emphasis is put on the general approach and applicability of typical process calculus methods, referring to the traditional comparison between abstract high-level black-box specifications with concrete low-level white-box implementations, using notions of equivalence or congruence,
respectively. A number of verification examples are presented; their advantages and disadvantages as well as potential pitfalls are outlined.

Speaker: Einar Broch Johnsen
Title: Open distributed systems: an executable OO model
We present an overview of the Creol language, an object-oriented modeling language for open distributed systems. The language, based on concurrent objects, addresses distribution by asynchronous method calls, delegation by first-class futures, and openness by a dynamic class construct which allow class definitions to evolve at runtime. Creol is an executable modeling language; i.e., although it is executable, its execution is highly nondeterministic. Specifically, it abstracts from particular network properties and allows local computation to adapt to the delays of the environment by an underspecified local scheduling. The language is statically typed, has a semantics defined in rewriting logic, and executes on the Maude system.

Speaker: Naoki Kobayashi
Title: Type-Based Analysis of Concurrent Programs
In this talk, I give a general overview of type systems for concurrency. After a short survey of the history and state-of-the-art of type systems for concurrency, I demonstrate TyPiCal, a type-based static analyzer for the pi-calculus.I conclude the talk with discussion on emerging and future research issues in this research field.

Speaker: Wolfgang Reisig
Title: Service modeling from scratch
The paradigm of "Service-oriented Computing" provides a framework for interorganizational business processes and for the emerging ideas of "programming in-the-large". Services are to be comprehensible without reference to implementation details. Interaction of services is established by their composition. This gives rise to a number of problems:

- Are two services partners, i.e. do they properly compose?
- Does a service have partners at all (otherwise, it is definitely ill-designed)?
- How to characterize all partners of a service?
- How to represent an operating guideline for a service?
- Is there a canonical (most liberal) partner of a service?
- Can a service S' substitute a service S?
- Is there a canonical (most abstract) S' to substitute S?
- Can S' substitute S at runtime?
- How to adapt (i.e. mediate between) two services that "almost" properly compose?

Such issues can be discussed by means of models of services. We show how services can intelligibly be modelled, and we discuss algorithms and tools to analyze the above mentioned problems.

Speaker: P. Madhusudan
Title: Analysing heaps using automata
We survey various mechanisms that automata theory provides in software
verification, including the logic-automata connection, modeling recursive control using (visibly) pushdown automata, algorithmic learning of regular languages, monitoring using deterministic automata, and deciding properties of graphs using automata and tree interpretations. We give a brief overview of work by the speaker in using the above in software verification--- the theory of visibly pushdown automata, logics and model-checking for pushdown systems, applying learning to infer method-call interfaces to
Java code and in compositionally verifying systems, and monitoring concurrent programs for atomicity using deterministic automata.

We also propose a new application of automata and the theory of decidable graph classes using tree interpretations: analysing heap invariants in programs.We present a preliminary study that is a general abstraction-refinement paradigm based on automata based shapes to capture invariants.

Speaker: Marino Miculan
Title: Directed bigraphs - a metamodel for communication, mobility and resources
The plethora of calculi and models of concurrent systems motivate the research for general metamodels, i.e., frameworks, for describing uniformly as many computational paradigms as possible. In this talk we discuss "directed bigraphs", a bigraphical metamodel in the line of Milner's bigraphs, intended to express the aspects of distributed computing such as communications, location, mobility and resources. The key novelty with respect to other variants of bigraphs (which are subsumed), is that directed bigraphs take account of the ?resource request flow? from controls to edges (through names). Directed bigraphs support a general construction (called IPO construction) for deriving labelled transition systems from (possibly open) reactive systems; remarkably, these bisimulations are always congruences. After having presented the formalism, we exemplify the encoding methodology by showing how the lambda-calculus and the fusion calculus are represented.

Speaker: Thao Dang
Title: Coverage-guided test generation for hybrid systems
Hybrid systems have been recognized as a high-level model appropriate for embedded systems, since this model can describe, within a unified framework, the logical part and the continuous part of an embedded system. Due to the gap between the capacity of exhaustive formal verification methods and the complexity of embedded systems, testing is still the most commonly-used validation method in industry. Its success is probably due to the fact that testing suffers less from the `state explosion' problem. Since it is impossible to enumerate all the admissible external inputs to the hybrid system in question, much effort has been invested in defining and implementing notions of coverage that guarantee, to some extent, that the finite set of input stimuli against which the system is tested is sufficient for validating correctness. For discrete systems, specified using programming languages or hardware design languages, some syntactic coverage measures can be defined, like exercising every statement or transition, etc. In this work, we treat continuous and hybrid systems that operate in a metric space and where there is not much inspiration coming from the syntax to the coverage issue. On the other hand, the metric nature of the state space encourages more semantic notions of coverage, namely that all system trajectories generated by the input test patterns form a kind of dense network in the reachable state space without too many big unexplored `holes'.

In this work we adopt a model-based testing approach. We propose a test coverage measure for hybrid systems, which is defined using the star discrepancy notion from statistics. This coverage measure is used to quantify the validation `completeness'. It is also used to guide input stimulus generation by identifying the portions of the system behaviors that are not adequately examined. We propose an algorithm for generating tests from hybrid systems models, which is based on the RRT (Rapidly-exploring Random Tree) algorithm from robotic motion planning and guided by the coverage measure. We also present an implementation of the algorithm and some experimental results on a number of case studies from control systems and analog and mixed-signal circuits.

Speaker: Ahmed Bouajjani
Title: Automata-based techniques for the verification of programs with dynamic linked data structures

(joint work with Peter Habermehl, Pierre Moro, Adam Rogalewicz, and Tomas Vojnar)

Abstract: We propose an approach for the automatic analysis of programs with dynamic linked structures using finite-state word/tree automata as representations for (potentially infinite) sets of heap structures. A heap of a given program is encoded as a word or a tree over an appropriate alphabet, and each statement in the program is translated into a transducer (I/O automaton) defining a transformation on the heap encodings. Then, iterative reachability analysis is performed using automata techniques in order to compute an upper-approximation of the set of all reachable heap configurations. The reachability analysis uses abstractions on automata representations (corresponding to finite index equivalence relations on their state space) allowing to speed up the fixpoint computation and to force termination. Automatic abstraction refinement is applied by need based on counterexample analysis. The proposed approach has been implemented and applied on various non trivial examples of programs.

Speaker: Christel Baier
Title: Probabilistic Buechi Automata

Speaker: Wojciech Penczek
Title: Model Checking of (Timed) Security Protocols
In this talk we offer a novel methodology for verifying correctness of (timed) security protocols. The idea consists in computing the time of a correct execution of a session and finding out whether the Intruder can change it to shorter or longer by an active attack.Moreover, we generalize the correspondence property so that attacks can be also discovered when some time constraints are not satisfied. An implementation of our method is discussed. As case studies we verify generalized (timed) authentication of Kerberos, TMN, Neumann Stubblebine Protocol, Andrew Secure Protocol, Wide Mouthed Frog, and NSPK.

Speaker: Catuscia Palamidessi
Title: Formal approaches to Information-hiding - An overview

(Partly based on joint work with Konstantinos Chatzikokolakis and Prakash Panangaden)

Abstract: We give an overview of various formal approaches from literature to information-hiding: The possibilistic approaches, the probabilistic approaches, the information-theoretic approaches, and the one based on statistical inference. We compare the various frameworks and point out the relations. Finally, we show how to specify information-hiding protocols and verify them (in the various approaches) using language- based techniques.

Speaker: Antonin Kucera
Title: Quantitative analysis of probabilistic pushdown automata
Probabilistic pushdown automata are obtained from "ordinary" non-deterministic PDA by attaching probabilities to transitions. Thus, each probabilistic PDA determines a discrete-time Markov chain with infinitely many states. We present selected constructions
and proof techniques that have recently been used to solve some natural problems of quantitative analysis of probabilistic PDA.

Speaker: R. Ramanujam
Title: A logic for strategies
The analysis of non-zero-sum games proceeds by determining the response of players to opponents' strategies. However, this requires each player to know what every other player would do in every possible situation, which is quite unrealistic in large games. We look at situations where players construct bounded memory strategies in a structured manner, where the opponent's strategy may be known only by its properties. In the new setting we study the algorithmic question of finding best response for a player.

We also present a simple modal logic to reason about strategies and show that checking assertion on a game graph is decidable.

Speaker: Frank de Boer
Title: Tasks for Actors

Speaker: Eike Best
Title: Separability, and other Equivalence Results
The following four results were briefly discussed:
that bounded Petri nets can be transformed into pomset-equivalent safe nets;
that live and bounded marked graphs can be transformed into step-equivalent live and safe marked graphs;
that safe labelled marked graphs can be transformed into pomset-equivalent tau-free safe labelled marked graphs;
and that marked graphs can be separated.

Two open problems that have arisen in this context were also mentioned, namely: can every safe labelled Petri net be transformed into a pomset-equivalent tau-free safe labelled
Petri net; and are live and bounded persistent nets separable?


Eike Best, Philippe Darondeau, and Harro Wimmel:
Making Petri Nets Safe and Free of Internal Transitions.Fundamenta Informaticae 80(2007), 1-16.

Speaker: Marcelo Frias
Title: Combining Lightweight and Heavyweight Formal Methods
The talk contained two main contributions. On the theoretical side, it presented a novel complete proof calculus for Alloy. On the applied side we presented Dynamite, a tool that combines the semi-automatic theorem prover PVS with the Alloy Analyzer. Dynamite allows one to prove an Alloy assertion from an Alloy specification using PVS, while using the Alloy Analyzer for the automated analysis of hypotheses introduced during the proof process.

Speaker: Luis Caires
Title: Logical Semantics of Types for Concurrency
The subject-reduction proof method to the soundness of type systems turned out to be very successful and applicable to many kinds of programming languages, in particular, to concurrent process calculi. Nevertheless, it appears to have contributed in the long term to widespread a too syntactic understanding of types and typing, rather far from the original and more natural semantic view of types as properties or predicates.

In this talk, we motivate a logical semantic approach to types for concurrency and to the soundness of related systems. The approach is illustrated by the development of a generic type system for the pi-calculus, which may be instantiated for specific notions of typing
by extension with adequate subtyping principles. Soundness of our type system is established using a logical predicate technique, based on a compositional spatial logic interpretation of types. This development gives some evidence that the intensional character of behavioral-spatial logics seems rather adequate for the characterization of several common type-like properties.