IFIP WG 2.2 Meeting Torino

September 12-14, 2008

Titles and abstracts for talks

(in chronological order)

Speaker: Andrzej Tarlecki
Title: Heterogeneous Logical Environments: an Institutional View

Abstract:
We work within the theory of institutions as a framework where the theory of specification and formal software development may be presented in an adequately general and abstract way. As differentlogical systems may be appropriate or most convenient for specification of different modules of the same system, of different aspects of system behaviour, or of different stages of system development, we need a number of logical systems to be used in the same specification and development project. This motivates the presented research on heterogeneous logical environments and specifications built in such environments.

We formalise logical systems as institutions. To enable a sensible use of a number of institutions together, in heterogeneous logical environments we link them with each other by institution morphisms or other maps between institutions, like institution comorphisms. Using them together with other standard (intra-institutional) specification-building operations, one builds heterogeneous structured specifications, which may involve a number of institutions to specify some aspects or some parts of the system, but ultimately focus at one institution of interest.

One family of logical systems is suggested by UML, where system specifications typically involve a number of diagrams of different kinds, each capturing a different aspect of the system. Each kind of UML diagrams leads to a separate logical system which, at least in principle, can be formalised as an institution. Expected relationships between system properties specified by different kinds of UML diagrams may now be captured using appropriate institution maps. UML specifications, however, are quite different from focused heterogeneous specifications mentioned above. They just form a collection of specifications residing in different institutions of UML diagrams.

We present a general abstract concept of a distributed heterogeneous specifcations that consist of a collection of specifications focused at various institutions in an underlying heterogeneous logical environment, linked by specification morphisms generalised by involving institution maps.  Distributed heterogeneous specifications come equipped with a rather natural semantics, given in terms of compatible families of models of component specifications. This yields in the standard way a number of usual concepts: consistency, semantic consequence, and perhaps most importantly, implementation of one distributed specification by another.

Each basic concept of a map between institutions can be captured by institution (co)morphisms --- as a span of (co)morphisms.  Replacing a map between institutions by an appropriate span of (co)morphisms allows one to represent exactly the same relationship between institutions and their components.  However, the categories of specifications that emerge in each case are different. Nevertheless, we argue that the expressive power of distributed specicfications built over them does not essentially differ.

based on joint work with
TILL MOSSAKOWSKI
MARIA VICTORIA CENGARLE, ALEXANDER KNAPP, MARTIN WIRSING

Speaker: Ernst Ruediger Olderog
Title: Explicit Fair Scheduling for Dynamic Control

Abstract:
In explicit fair schedulers, auxiliary integer-valued scheduling variables with non-deterministic assignments and with decrements keep track of each processor's relative urgency.

Every scheduled execution is fair and yet, the scheduler is sufficiently permissive (every fair run can be scheduled).

We investigate whether explicit fair scheduling also works with dynamic control, i.e., when new processes may be created dynamically.

We give a positive and a negative answer.

Speaker: Marcelo Frias
Title: Distributed Analysis of Relational Models

Abstract:
In this talk I present ParAlloy, a tool for the distributed analysis of relational models that allows us to analyze models that largely exceed the current capabilities of the sequential tools available.

Joint work with Nicolas Rosner and Carlos Lopez Pombo

Speaker: Herbert Wiklicky
Title: Leaks: How to Avoid, Fix and/or Measure

Abstract:
We present an overview over approaches in language-based security related to the problem of covert channels, i.e. unauthorised information flow. This concerns the work by Volpano, Smith et.al. on types for secure information flow analysis and Agat's program transformation for fixing so-called timing-leaks which is based on the Volpano-Smith type system. We then describe a new notion of security against timing attacks where the attacker is able to simultaneously observe the execution time of a program and the probability of the values of low variables. Finally, we introduce a probabilistic version of Agat's transformation which we use to analyse the trade-off between gain in (approximate) security and additional (running time) costs.

Literature

D.Volpano, G.Smith and C.Irvine: A Sound Type System for Secure Flow Analysis, JCS 4(3), 1996.

J.Agat: Transforming Out Timing Leaks, POPL'00.

A. Di Pierro, C. Hankin, and H. Wiklicky: Quantifying Timing Leaks and Cost Optimisation, ICICS 2008, LNCS 5308 (cf also arXiv:0807.3879).

joint work with A. Di Pierro and C. Hankin

Speaker: Naoki Kobayashi
Title: Type Systems for Program Analysis

Abstract:
Since linear logic was proposed by Girard, a number of type systems inspired by linear logic (or substructural logics in general) have been proposed.  Examples include linear type systems, where the weakening and contraction rules are restricted, and ordered type systems, where the exchange rule is also restricted.  Those type systems turned out to be very useful for reasoning about temporal properties of programs, like a memory cell is deallocated only once, or a memory cell is never read or written after it is deallocated.  In this talk, I will focus on substructural type systems for program analysis, and review their principles and applications.  I will also discuss some emerging techniques and future directions of substructural-type-based program analysis.

Speaker: Einar Broch Johnsen
Title: Lazy Behavioural Subtyping

Abstract:
Late binding allows flexible code reuse but complicates formal reasoning significantly, as a method call's receiver class is not statically known. This is especially true when programs are incrementally developed by extending class hierarchies.  This paper develops a novel method to reason about late bound method calls.  In contrast to traditional behavioral subtyping, reverification is avoided without restricting method overriding to fully behavior-preserving redefinition.  The approach ensures that when analyzing the methods of a class, it suffices to consider that class and its superclasses.  Thus, the full class hierarchy is not needed, and incremental reasoning is supported.  We formalize this approach as a calculus which lazily imposes context-dependent subtyping constraints on method definitions.  The calculus ensures that all method specifications required by late bound calls remain satisfied when new classes extend a class hierarchy.  The calculus does not depend on a specific program logic, but the examples use a Hoare-style proof system. We show soundness of the analysis method.

The talk builds on the paper

Johan Dovland, Einar Broch Johnsen, Olaf Owe, and Martin Steffen
Lazy Behavioral Subtyping
Proc. 15th Intl. Symposium on Formal Methods (FM'08), pp. 52-67.
LNCS 5014. Springer 2008.

Speaker: Simona Ronchi della Rocca
Title: Languages with bounded computational complexity

Abstract:
Starting from Soft Linear Logic, characterizing polynomial time complexity, we design
three type assignment systems for (extensions of) the lambda calculus, where the existence of a typing for a term guarantees a bound on the complexity of its reduction to normal form. The considered complexity classes are (F)PTIME, PSPACE and NPSPACE. The type assignments are also complete for the related complexity class, in the sense that every function with the given complexity is representable by a well typed term. A discussion will follow on the open problems and future work.

Speaker: Masahiko Sato
Title: External and Internal Syntax of Lambda Calculus

Abstract:
It is well known that defining the substitution operation on $\lambda$-terms appropriately and establish basic properties like the substitution lemma is a subtle task if we wish to do it formally. The main obstacle here comes from the fact that unsolicited capture of free variables may occur during the substitution if one defines the operation naively. We argue that although there are several approaches to cope with this problem, they are all unsatisfactory since each of them defines the $\lambda$-terms in terms of a single fixed syntax. We propose a new way of defining $\lambda$-terms which uses an external syntax to be used mainly by humans and an internal syntax which is used to implement $\lambda$-terms on computers. The $\lambda$-terms of both the internal and the external syntax will be defined as subsets of a same set of symbolic expressions. We introduce a new algebraic structure called {\it B-algebra} and the set of symbolic expressions will be defined as a free B-algebra. In this setting, we will show that we can define $\lambda$-terms and the substitution operation naturally and can establish basic properties of terms easily. A draft of the paper is available at: (http://www.sato.kuis.kyoto-u.ac.jp/~masahiko/research-e.html )

Speaker: Willem-Paul de Roever
Title: A Perspective on Program Verification

Abstract:
The talk describes how I look back on being active for 38 years in the field of Program Verification. In its first part I describe how I have filled in my professional activities, namely,

(I) By promoting research and giving courses in Program Verification and Program Semantics, including the writing of two textbooks: (1)  Data Refinement (which will be published in pocket version this year), and (2) Concurrency Verification, both published by Cambridge  University Press.
(II) By organizing Conferences, Workshops,  and Schools, in order to help establishing a community.
(III) By organizing approximately 25 International and national Third-  Party Projects, of which 7 supported by the EU, in order to establish a critical mass of active researchers in Europe in the field of Program Verification.

In its second part I analyze which obstacles have to be overcome before software verified upon its correctness is an accepted product.

Finally, in its third part I make a prediction,  based on an analogy with the development of reliable steam engines, reliable cars, reliable airplanes and reliable computers (i.e., the four driving forces behind man's  technological revolution), of when reliable software will become an accepted commodity: 2035, and explain why I am that optimistic.

Speaker: Naoki Kobayashi
Title: Type-Based Analysis of Concurrent Programs

Abstract:
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: Ahmed Bouajjani
Title: On the Automatic Verification of Dynamic / Parametrized Systems

Abstract:
We give an overview on automatic verification of infinite-state systems in general and in particular of dynamic/parametrized networks of processes. We present (some of) the main existing approaches based on symbolic techniques with automata/logic based formalisms for the representation of infinite sets of configurations, and methods and techniques for ensuring/helping termination of the analysis. We show the application of the presented techniques in the verification of various classes of systems/programs (such as concurrent programs with dynamic creation of processes, networks of timed systems, programs with dynamic heaps,programs with arrays, etc.).

Speaker: Luis Caires
Title: Concurrency Control Types for Object-Oriented Programming

Abstract:
We discuss programming language abstractions and types for statically enforcing safe concurrency in object-oriented programs. More precisely, our types express dynamic concurrency control constraints by freely combining parallel / sequential / sharing / ownership operators. We show through a sequence of simple yet illuminating examples how our type system may statically ensure absence of common errors in general concurrent / distributed programs. To conclude, we will argue that our encourages the programmer to think in terms of behavioral, separation, and
ownership invariants, rather than in (naive) terms of lock acquisition and control flow.

Speaker: Sophia Drossopoulou
Title: Design and Formalization of Object Oriented Language Features

Abstract:
I presented some of my work on oo programming language specification and design, as well as the lessons learnt on the way. I started with the formalization and proof of type soundness of large subsets of Java, in particular intricacies wrt to overloading,
http://pubs.doc.ic.ac.uk/JavaTypeSystemSoundTaPOS/
I then discussed issues around Java dynamic lining, binary compatibility, and the very weak guarantees made by separate compilation.
http://pubs.doc.ic.ac.uk/FragmentCalculus/
Ownership and universe types characterize objects in terms of "boxes", a hierarchical heap topology,
http://pubs.doc.ic.ac.uk/ownershipAndEffects/
http://pubs.doc.ic.ac.uk/multiple-ownership/
which may be used for memory management, garbage collection, and program verification. Interestingly, the meaning of types in such systems is relative to some observer object, or to a stack (the current this). More recently, work on soundness of Java wildcards
http://pubs.doc.ic.ac.uk/wildcards-ecoop-08/
has thrown interesting questions about models for types and subtyping.

List of papers at    http://pubs.doc.ic.ac.uk/authors/scd/

Speaker: Antonin Kucera
Title: Properties of Stochastic Games with Branching-Time Objectives

Abstract:
Stochastic games are directed binary graphs where each vertex belongs either to Player-I, Player-II, and it is stochastic. The talk surveys recent results about stochastic games with branching-time winning objectives that are specified as formulae of probabilistic branching-time logics such as PCTL or PCTL*. The goal of Player-I is to satisfy a given formula, while Player-II aims at the opposite. Such games are generally not determined, and winning strategies (if they exist) may require both memory and randomization. Still, the winner in such games can be determined effectively in some cases.

References:

T. Brázdil, V. Forejt, and A. Kučera.
Controller Synthesis and Verification for Markov Decision Processes with
Qualitative Branching Time Objectives.
In Proceedings of 35th International Colloquium on Automata, Languages and
Programming (ICALP 2008), pages 148-159, volume 5126 of LNCS. Springer,
2008.

T. Brázdil, V. Brožek, V. Forejt, and A. Kučera.
Stochastic Games with Branching-Time Winning Objectives.
In Proceedings of 21st Annual IEEE Symposium on Logic in Computer
Science (LICS 2006),
pages 349-358, IEEE Computer Society, 2006.

(a joint work with Tomáš Brázdil and Vojtěch Forejt)

Speaker: Luke Ong
Title: Model-checking multithreaded programs: an automata-theoretic approach

Abstract:
We survey the model-checking approach to the verification of multithreaded programs. Each thread is assumed to be the computation of a WHILE program. We consider a number of computational scenarios in which one or more of the following features are present:

(R) Each thread is a generalized Boolean program i.e. it has recursively defined procedures

(C) Threads may communicate by shared resources (i.e. global variables)

In general the key analysis problem of Reachability is undecidable. We survey different approaches to approximating Reachability.

Speaker: Eike Best
Title: A Decomposition Theorem for Finite Persistent Transition Systems

Abstract:
We consider finite labelled transition systems and show that if such transition systems are deterministic, persistent, and weakly periodic, then they can be decomposed in the sense that there exists a finite set of label-disjoint cycles such that any other cycle is Parikh-equivalent
to a multiset of cycles from this set. We also show that as a consequence, bounded, persistent and reversible Petri nets are amenable to modular verification.

(joint work with Philippe Darondeau)

Speaker: Roland Meyer
Title: A Structural Petri Net Semantics for the Pi Calculus

Abstract:
Automata-theoretic representations have proven useful in the automatic and exact analysis of computing systems. We propose a new semantical mapping of $\pi$-Calculus processes into place/transition Petri nets. Our translation reflects the structure of processes, which is induced by the use of restricted names. The property of structural stationarity characterises the processes mapped to finite nets. Different from our approach, classical Petri net semantics reflect the concurrency of sequential processes. They finitely represent a class of processes that is incomparable with structurally stationary processes. By typing restricted names, the structural and the concurrency semantics can be combined. This combination gives rise to a hierarchy of processes into which we sort the related work of Dam, Engelfriet, Montanari, Caires, Koutny, Busi, Gorrieri, Amadio, and Meyssonnier.

Speaker: Igor Walukiewicz
Title: Some remarks on expressing tree properties

Abstract:
We see trees in almost any part of computer science. Traditionally, ranked trees, that are nothing else but terms, captured most attention, although exceptions could have been found in graph theory or linguistics. Recently, unranked trees are a subject of renewed interest.

We discuss two curious topics concerning formalism expressing tree properties. The first is order invariance: what properties can be expressed with order between siblings but cannot be expressed without it. In case of monadic second-order logic, we known that these are  precisely counting modulo properties. The first-order case is open. The other topic is that of finite base. Kamp's theorem says that over words first-order logic is equivalent to linear time temporal logic. The later is a modal logic with a finite number of additional operators. It turns out that one cannot have the same result for trees. To capture a reasonably simple class of first-order definable
languages we need an infinite number of operators, or backward  modalities.

Speaker: Rocco De Nicola
Title: Session Centered Calculi for Service-Oriented Computing

Abstract:
Within the European project SENSORIA, we are developing formalisms for service description that lay the mathematical basis for analysing and experimenting with components interactions, for combining services and
formalising crucial aspects of service level agreement. One of the outcome is CaSPiS, a name passing process calculus with explicit notions of service definition, service invocation and bi-directional sessioning that supports explicit modeling of sessions both on client- and on service-side Sessions permit describing and reasoning about interaction modalities more structured than the simple one-way and request-response modalities and typical of a producer / consumer pattern. The calculus is also equipped with operators for handling (unexpected) session closures that permit programming smooth propagation of session closures to partners and subsessions, so as to avoid states with dangling or orphan sessions. In the talk we have presented CaSPiS and discuss other alternatives that are (have been) considered within the project.

Speaker: Wojciech Penczek
Title: Model checking security protocols: a multi-agent system approach

Abstract:
We present a formalism for the automatic verification of security protocols based on multi-agent systems semantics. We give the syntax and semantics of a temporal-epistemic security specialised logic and provide a lazy-intruder model for the protocol rules that we argue to be particularly suitable for verification purposes. We exemplify the technique by finding a (known) bug in the traditional NSPK protocol.

Availalbe from http://www.ipipan.waw.pl/~penczek/Slajdy/wg22-2008.pdf
Published in Fundamenta Informaticae Volume 85, Number 1-4, pp. 359-375, 2008.

Speaker: Ugo Montanari

Title: Symbolic Semantics Revisited
Abstract:
Symbolic bisimulations were introduced as a mean to define value-passing process calculi using smaller, possibly finite labelled transition systems, equipped with symbolic actions. Similar ideas have been used for modeling with fewer transitions the input behavior
of open and asynchronous pi-calculus. In this paper we generalize the symbolic technique and apply the resulting theory to these two cases, re-deriving existing results. We also apply our approach to new settings, i.e. open Petri nets and cc-pi (concurrent constraint
pi-calculus), with the usual result of reducing input transitions.

(Joint work with Filippo Bonchi)

Speaker: Paola Giannini
Title: Type Safe Oriented Languages Supporting Dynamic Software Evolution

Abstract:
In the presentation I outline recent work on providing a foundation for expressing dynamic object oriented language features such as: multidimensional dispatch (dispatch not only on receiver, but also sender, contextual information, etc.), context oriented programming
fine grain (static and dynamic) extension of class behaviour with traits. Such work will be compared with similar ideas that have been used in more  applicative areas.

Speaker: Maciej Koutny
Title: Steps and Coverability in Inhibitor Nets

Abstract:
For Petri nets with inhibitor arcs, properties like reachability and boundedness are undecidable and hence constructing a coverability tree is not feasible. In recent work we investigated to what extent the coverability tree construction might be adapted for Petri nets with inhibitor arcs. Emphasis was given to the (a priori) step sequence semantics which cannot always be simulated by firing sequences. All this led to the notion of a step coverability tree which may be of use for the analysis of the step behaviour of certain subclasses of Petri nets with  inhibitor arcs.

(joint work with Jetty Kleijn)