LNCS 4424_ Tools and Algorithms for the Construction and Analysis of Systems [Grumberg & Huth 2007-04-12].pdf

(8806 KB) Pobierz
Lecture Notes in Computer Science
Commenced Publication in 1973
Founding and Former Series Editors:
Gerhard Goos, Juris Hartmanis, and Jan van Leeuwen
4424
Editorial Board
David Hutchison
Lancaster University, UK
Takeo Kanade
Carnegie Mellon University, Pittsburgh, PA, USA
Josef Kittler
University of Surrey, Guildford, UK
Jon M. Kleinberg
Cornell University, Ithaca, NY, USA
Friedemann Mattern
ETH Zurich, Switzerland
John C. Mitchell
Stanford University, CA, USA
Moni Naor
Weizmann Institute of Science, Rehovot, Israel
Oscar Nierstrasz
University of Bern, Switzerland
C. Pandu Rangan
Indian Institute of Technology, Madras, India
Bernhard Steffen
University of Dortmund, Germany
Madhu Sudan
Massachusetts Institute of Technology, MA, USA
Demetri Terzopoulos
University of California, Los Angeles, CA, USA
Doug Tygar
University of California, Berkeley, CA, USA
Moshe Y. Vardi
Rice University, Houston, TX, USA
Gerhard Weikum
Max-Planck Institute of Computer Science, Saarbruecken, Germany
Orna Grumberg Michael Huth (Eds.)
Tools and Algorithms
for the Construction
andAnalysis of Systems
13th International Conference, TACAS 2007
Held as Part of the Joint European Conferences
on Theory and Practice of Software, ETAPS 2007
Braga, Portugal, March 24 - April 1, 2007
Proceedings
13
Volume Editors
Orna Grumberg
Technion
Israel Institute of Technology
Haifa 32000, Israel
E-mail: orna@cs.technion.ac.il
Michael Huth
Imperial College London
United Kingdom
E-mail: M.Huth@doc.imperial.ac.uk
Library of Congress Control Number: 2007922076
CR Subject Classification (1998): F.3, D.2.4, D.2.2, C.2.4, F.2.2
LNCS Sublibrary: SL 1 – Theoretical Computer Science and General Issues
ISSN
ISBN-10
ISBN-13
0302-9743
3-540-71208-9 Springer Berlin Heidelberg New York
978-3-540-71208-4 Springer Berlin Heidelberg New York
This work is subject to copyright. All rights are reserved, whether the whole or part of the material is
concerned, specifically the rights of translation, reprinting, re-use of illustrations, recitation, broadcasting,
reproduction on microfilms or in any other way, and storage in data banks. Duplication of this publication
or parts thereof is permitted only under the provisions of the German Copyright Law of September 9, 1965,
in its current version, and permission for use must always be obtained from Springer. Violations are liable
to prosecution under the German Copyright Law.
Springer is a part of Springer Science+Business Media
springer.com
© Springer-Verlag Berlin Heidelberg 2007
Printed in Germany
Typesetting: Camera-ready by author, data conversion by Scientific Publishing Services, Chennai, India
Printed on acid-free paper
SPIN: 12029204
06/3142
543210
Foreword
ETAPS 2007 is the tenth instance of the European Joint Conferences on Theory
and Practice of Software, and thus a cause for celebration.
The events that comprise ETAPS address various aspects of the system de-
velopment process, including specification, design, implementation, analysis and
improvement. The languages, methodologies and tools which support these ac-
tivities are all well within its scope. Different blends of theory and practice
are represented, with an inclination towards theory with a practical motivation
on the one hand and soundly based practice on the other. Many of the issues
involved in software design apply to systems in general, including hardware sys-
tems, and the emphasis on software is not intended to be exclusive.
History and Prehistory of ETAPS
ETAPS as we know it is an annual federated conference that was established
in 1998 by combining five conferences [Compiler Construction (CC), European
Symposium on Programming (ESOP), Fundamental Approaches to Software En-
gineering (FASE), Foundations of Software Science and Computation Structures
(FOSSACS), Tools and Algorithms for Construction and Analysis of Systems
(TACAS)] with satellite events.
All five conferences had previously existed in some form and in various colo-
cated combinations: accordingly, the prehistory of ETAPS is complex. FOSSACS
was earlier known as the Colloquium on Trees in Algebra and Programming
(CAAP), being renamed for inclusion in ETAPS as its historical name no longer
reflected its contents. Indeed CAAP’s history goes back a long way; prior to
1981, it was known as the Colleque de Lille sur les Arbres en Algebre et en
Programmation. FASE was the indirect successor of a 1985 event known as Col-
loquium on Software Engineering (CSE), which together with CAAP formed a
joint event called TAPSOFT in odd-numbered years. Instances of TAPSOFT, all
including CAAP plus at least one software engineering event, took place every
two years from 1985 to 1997 inclusive. In the alternate years, CAAP took place
separately from TAPSOFT.
Meanwhile, ESOP and CC were each taking place every two years from 1986.
From 1988, CAAP was colocated with ESOP in even years. In 1994, CC became
a “conference” rather than a “workshop” and CAAP, CC and ESOP were there-
after all colocated in even years.
TACAS, the youngest of the ETAPS conferences, was founded as an inter-
national workshop in 1995; in its first year, it was colocated with TAPSOFT. It
took place each year, and became a “conference” when it formed part of ETAPS
1998. It is a telling indication of the importance of tools in the modern field of
informatics that TACAS today is the largest of the ETAPS conferences.
VI
Foreword
The coming together of these five conferences was due to the vision of a small
group of people who saw the potential of a combined event to be more than the
sum of its parts. Under the leadership of Don Sannella, who became the first
ETAPS steering committee chair, they included: Andre Arnold, Egidio Aste-
siano, Hartmut Ehrig, Peter Fritzson, Marie-Claude Gaudel, Tibor Gyimothy,
Paul Klint, Kim Guldstrand Larsen, Peter Mosses, Alan Mycroft, Hanne Riis
Nielson, Maurice Nivat, Fernando Orejas, Bernhard Steffen, Wolfgang Thomas
and (alphabetically last but in fact one of the ringleaders) Reinhard Wilhelm.
ETAPS today is a loose confederation in which each event retains its own
identity, with a separate programme committee and proceedings. Its format is
open-ended, allowing it to grow and evolve as time goes by. Contributed talks
and system demonstrations are in synchronized parallel sessions, with invited
lectures in plenary sessions. Two of the invited lectures are reserved for “uni-
fying” talks on topics of interest to the whole range of ETAPS attendees. The
aim of cramming all this activity into a single one-week meeting is to create a
strong magnet for academic and industrial researchers working on topics within
its scope, giving them the opportunity to learn about research in related areas,
and thereby to foster new and existing links between work in areas that were
formerly addressed in separate meetings.
ETAPS 1998–2006
The first ETAPS took place in Lisbon in 1998. Subsequently it visited Ams-
terdam, Berlin, Genova, Grenoble, Warsaw, Barcelona, Edinburgh and Vienna
before arriving in Braga this year. During that time it has become established
as the major conference in its field, attracting participants and authors from
all over the world. The number of submissions has more than doubled, and the
numbers of satellite events and attendees have also increased dramatically.
ETAPS 2007
ETAPS 2007 comprises five conferences (CC, ESOP, FASE, FOSSACS, TACAS),
18 satellite workshops (ACCAT, AVIS, Bytecode, COCV, FESCA, FinCo, GT-
VMT, HAV, HFL, LDTA, MBT, MOMPES, OpenCert, QAPL, SC, SLA++P,
TERMGRAPH and WITS), three tutorials, and seven invited lectures (not in-
cluding those that were specific to the satellite events). We received around 630
submissions to the five conferences this year, giving an overall acceptance rate of
25%. To accommodate the unprecedented quantity and quality of submissions,
we have four-way parallelism between the main conferences on Wednesday for
the first time. Congratulations to all the authors who made it to the final pro-
gramme! I hope that most of the other authors still found a way of participating
in this exciting event and I hope you will continue submitting.
ETAPS 2007 was organized by the Departamento de Inform´tica of the Uni-
a
versidade do Minho, in cooperation with
Zgłoś jeśli naruszono regulamin