IFIP WG
2.2 Meeting
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
ADAM WARSKI
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
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
(D) A thread may spawn other threads - call it Dynamic
(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)