Some titles and abstracts for talks IFIP WG 2.2 Anniversary Meeting
(in alphabetical order)

Speaker: Egon Boerger
Title: Contributions of the Abstract State Machines method to program verification and some future challenges
We first survey applications of the ASM method for a rigorous definition and mathematical analysis of the semantics of modern programming languages and their implementation. Then we discuss some contributions the ASM method can provide to address the Verified Software Grand Challenge proposed by T. Hoare.

Speaker: Philippe Darondeau
Title: Petri net synthesis 10 years later
We survey results and applications found in the last decade in the field of Petri net synthesis. We present current trends of research and open problems.

Speaker: Mariangiola Dezani
Title: Session Types for Object-Oriented Languages
A session takes place between two parties; after establishing a connection, each interleaves local computations and communications (sending or receiving) with the other. Session types characterise such sessions in terms of the types of values communicated and the shape of protocols, and have been developed for the pi-calculus, CORBA interfaces, and functional languages. We study the incorporation of session types into object-oriented languages through MOOSE, a multi-threaded language with session types, thread spawning, iterative and higher-order sessions. Our design aims to consistently integrate the object-oriented programming style and sessions, and to be able to treat various case studies from the literature. We describe the design of MOOSE, its syntax, operational semantics and type system, and develop a type inference system. After proving subject reduction, we establish the progress property: once a communication has been established, well-typed programs will never starve at communication points. (Joint work with Dimitris Mostrous, Nobuko Yoshida and Sophia Drossopoulou)

Speaker: Furio Honsell
Title: A Framework for Defining Logical Frameworks

Speaker: Maciej Koutny
Title: Verifying Mobile Systems Using Petri Net Unfoldings
To make formally express and analyse mobile systems feasible, process algebras - notably the pi-calculus - have been introduced and extensively studied. This talk will describe how one can apply Petri net unfoldings in order to alleviate the state space explosion problem when model checking systems expressed in the finite pi-calculus.

Speaker: Leslie Lamport
Title: A State Machine by any Other Name
Much of computer science is about state machines, known by a multitude of names: automata (Buchi, cellular, pushdown), machines (Mealy, Moore,Turing), programs, Petri nets, process algebras, and so on. What are the significant differences among them all? Are state machines all you need?

Speaker: Hans Langmaack
Title: Revival of ALGOL-Concepts in Program and Specification Languages
In recent years there have happened extensions of two very respected and widely used programming and specification languages: The extension from original, object oriented, flat Java 1996 to new Java 2000 with class nesting (Gosling, Joy, Steele, Bracha) and from basic Abstract State Machines ASMs 1986/90 to Turbo ASMs 2002 (Gurevich, Boerger, Stark). These extensions are well comparable to the much earlier transition from Fortran 1954/57 (Backus) and Algol58, 1958 (Perlis, Samelson, Paul) to Algol60, 1960 (Naur et al.). It is Algol60's concept of program structuring, information encapsulation and hiding by the help of nested, non-formal and formal procedures with their static scope semantics the revival of which we detect under quite different namings both in new Java and in Turbo ASM.

Speaker: Marino Miculan
Title: Modal Logics for Brane Calculus
The Brane Calculus is a calculus of mobile processes, in- tended to model the transport machinery of a cell system. We present the Brane Logic, a modal logic for expressing formally properties about systems in Brane Calculus. Similarly to previous logics for mobile ambients, Brane Logic has specific spatial and temporal modalities. Moreover, since in Brane Calculus the activity resides on membrane surfaces and not inside membranes, we need to add a specific logic (akin Hennessy-Milner's) for reasoning about membrane activity. We provide also a proof system for deriving valid sequents in Brane Logic, and a model checker for a decidable fragment.

Speaker: Ugo Montanari
Title: A Larger Viewpoint about Leifer and Milner's Reactive Systems
A systematic method for deriving bisimulation congruence from reduction rules has been proposed by Leifer and Milner, on turn inspired by Sewell. Also, the approach of observing contexts imposed on agents at each step has been proposed earlier by Montanari and Sassone, yielding the notion of dynamic bisimilarity. The basic idea of Leifer and Milner is to express minimality conditions for electing the context to be used among the (possibly infinite) ones that allow the agent to react. These conditions have been distilled by them in the notion of relative push-out (RPO) in a categories of reactive systems and made more general by Sassone, Sobocinski and Lack. The RPO construction is reminiscent of the unification process of logic programming, which in fact can be given an interactive semantics in much the same style. In the talk we present a short survey of the relevant work and describe some recent developments which allow to see this approach under a larger viewpoint. The first contribution observes contexts also for symbolic execution, suggesting applications to web service binding; the second tackles the weak case by taking advantage of the tile model; and the third uses cospan categories on adhesive categories, as suggested by Sassone, Sobocinski and Lack, for representing process calculi as graph transformation systems. As a last contribution, we then propose saturated semantics, a new class of equivalences, based on a weaker notion of observation and orthogonal to all the previous proposals, and we demonstrate the appropriateness of our semantics by means of two examples: logic programming and a subset of the open pi-calculus. Indeed, we show that our equivalences are congruences and that they coincide with logical equivalence and open bisimilarity respectively, while equivalences studied in previous work are strictly finer (Joint work with Filippo Bonchi, Roberto Bruni, Gianluigi Ferrari, Fabio Gadducci, Barbara Koenig, Pawel Sobocinski and Emilio Tuosto).

Speaker: Peter D. Mosses
Title: Formal semantics online
Over the past 40 years, various formalisms for semantics have been developed - often by past or present members of WG 2.2 - and used to give semantic descriptions of some major programming languages. However, it appears that rather few semantic descriptions are currently available online. A comprehensive online archive of existing semantic descriptions would surely be a valuable resource in itself, and enhance the visibility of formal semantics in the computer science community. In this talk, we outline a new initiative to establish such an archive. We also consider the possibility of incorporating canonical descriptions of commonly-occurring individual constructs, which could serve as reusable components for future semantic descriptions.

Speaker: Ernst-Rudiger Olderog
Title: Automatic Verification of Combined Specifications
In our talk we report on the project "Beyond Timed Automata" (R1 for short) of the Collaborative Research Center AVACS (Automatic Verification and Analysis of Complex Systems) of the universities of Oldenburg, Freiburg, and Saarbr"ucken. AVACS is motivated by the challenge of automatically verifying safety properties of complex embedded systems like the European Train Control System (ETCS). The long term vision of R1 is to advance the automatic verification of high-level specifications in the dimensions of behaviour, data, and real-time. The current emphasis in R1 is on the automatic verification of specifications with infinite data and real-time constraints. In R1 we consider for the specifications of systems the language CSP-OZ-DC that combines three well researched specification techniques for processes, data and time: Communicating Sequential Processes (CSP), Object-Z (OZ), and Duration Calculus (DC). For the specifying real-time requirements we take the Duration Calculus. The combination CSP-OZ-DC has an operational semantics defined by J. Hoenicke in terms of Phase-Event-Automata (PEA). This semantics is compositional in the sense that the automaton describing the set of runs a combined CSP-OZ-DC specification is the parallel composition of the automata for the CSP part, the OZ part, and the DC part. Automatic verification of CSP-OZ-DC specifications is achieved using the Abstraction Refinement Model Checker (ARMC) of A. Rybalchenko. It uses transition constraint systems as input and can check the the reachability of set of states. In its current implementation it can handle constraints on data in the domains of real and integer numbers. PEA are very well suited as an intermediate language in translating CSP-OZ-DC specifications into transition constraint systems processed by ARMC. In the talk we illustrate the approach using the example of a parameterized elevator studied by J. Hoenicke and P. Maier. The point is that a safety property of the lift depending on real-time constraints in its CSP-OZ-DC specification can be proven automatically for arbitrarily many floors. Finally, we explain the status of a larger case study Emergency Messages of the ETCS. Acknowledgement. The project R1 is directed by A. Podelski, B. Finkbeiner, V. Sofroni-Stokkermans, and myself. The results reported in this talk build on further work of I. Br"uckner, J. Faber, J. Hoenicke, R. Meyer, P. Maier, A. Rybalchenko, S. Jacobs, and H. Wehrheim. For more information about AVACS see the web page

Speaker: Catuscia Palamidessi
Title: Anonymity Protocols as Noisy Channels
We propose a framework in which anonymity protocols are interpreted as particular kinds of channels, and the degree of anonymity provided by the protocol as the converse of the channel's capacity. We illustrate how several notions of anonymity can be expressed in this framework, and show the relation with various definitions of probabilistic anonymity in literature. (Joint work with Kostas Chatazikokolakis, Prakash Panangaden)

Speaker: Gordon Plotkin
Title: Origins of structural operational semantics

Speaker: Andrzej Tarlecki
Title: Toward (institutional) foundations for heterogeneous specifications
The overall idea of the talk is to present recent work aimed at dealing with multiple logical systems in a single specification and software development task. I first recall the basic technical notions related to modelling logical systems as institutions, and mention a number of exciting possibilities for applications of the theory of institutions. Then I sketch how the mechanisms of various mappings between institutions may be used to cater for heterogeneous specifications, which span an number of linked institutions, and for the description of the development process which may 'migrate' between various institutions in the course of development of separate modules of the system. I will introduce a concept of a distributed heterogeneous specification, which captures different views of the same system to be developed and briefly suggest how such distributed specifications can be used in the process of sofwtare development. Overall, a picture of a heterogeneous logical environment for software specification and development is emerging as a diagram of institutions linked by morphisms of various kinds.

Speaker: Igor Walukiewicz
Title: From logic to games
In this talk we will look at some developments in what is called formal verification. In the seventies logics occupied a principal place: Hoare logic, algorithmic logic, dynamic logic, linear time temporal logic. With a notable exception of the last one, these formalisms included programs into syntax of the logic with an idea to reduce verification to validity checking. Temporal logic was the first to advocate externalization of modeling of programs and passing from validity checking to model checking. Since the eighties, this view became predominant, and we have seen a proliferation of logical systems. On the way, we have learned that game based methods not only are very useful but also permit to abstract from irrelevant details of logical formalisms. At present games themselves take the place of specification formalisms.