Besides the five main conferences the following satellite events are planned for ETAPS 2002:
ACL2 is a state-of-the-art automated reasoning system, which grew out of the Boyer-Moore theorem prover and has been used successfully on a number of industrial and academic projects. The ACL2 workshop provides a forum for presentation and discussion of projects using ACL2 as well as evolution of the tool. The preceding workshops were held at the University of Texas in March 1999, resulting in two hard bound books, and October 2000, resulting in on-line proceedings accessible from the ACL2 home page. Papers are solicited on any topic related to ACL2, including but not limited to:
Contact: Matt Kaufmann, Advanced Micro Devices Inc, USA
E-mail: matt.kaufmann@amd.com
Web page: http://www.cs.utexas.edu/users/moore/acl2/workshop-2002
Graphs of all kinds are widely used to model complex states, structured objects, networks, and relational structures in many areas of computer science. Applied graph transformation is a rule-based framework for the specification and development of systems, languages, and tools that are founded on graphs. The area of graph transformation is supported by the ESPRIT Working Group APPLIGRAPH (Applications of Graph Transformation).
The APPLIGRAPH workshop is intended to bring together leading researchers in theory and application of graph transformation and researchers in other areas of ETAPS who are interested in graph transformation. For this reason, the workshop is not restricted to members of APPLIGRAPH, but open for anybody.
Main topics of interest include but are not limited to the following:
Contact: Hans-Joerg Kreowski, University of Bremen, Germany
E-mail: kreo@informatik.uni-bremen.de
Web page: http://www.informatik.uni-bremen.de/theorie/AGT2002
A great variety of state-based dynamical systems, like transition systems, automata, process calculi and class-based systems can be captured uniformly as coalgebras. Coalgebra is developing into a field of its own interest presenting a deep mathematical foundation, a growing field of applications and interactions with various other fields such as reactive and interactive system theory, object oriented and concurrent programming, formal system specification, modal logic, dynamical systems, control systems, category theory, algebra, analysis, etc. The aim of the workshop is to bring together researchers with a common interest in the theory of coalgebras and its applications.
Contact: Larry Moss, University of Indiana, USA
E-mail: lsm@cs.indiana.edu
Web page: http://www.cs.indiana.edu/cmcs
Semantics preservation between source and target program is the commonly accepted minimum requirement to be ensured by compilers. It is the key term compiler verification and optimization are centered around. The precise meaning, however, is often only implicit. Verification tends to interpret semantics preservation in a very tight sense, not only but also to simplify the verification task. Optimization prefers generally a more liberal view in order to enable more powerful transformations otherwise excluded. The surveyor's rod of admissibility is semantics preservation. Fundamental for this is the language semantics. But the adequate interpretation varies fluently with the application context ("stand-alone" programs, communicating systems, reactive systems, etc.).
The aim of the workshop is to bring together researchers and practitioners working on optimizing and verifying compilation, on language design and programming language semantics in order to plumb the degrees of freedom optimizers and verifiers have, to bridge the gap between the two communities, and to stimulate synergies.
Contact: Jens Knoop, University of Dortmund, Germany
E-mail: knoop@ls5.cs.uni-dortmund.de
Web page: http://sunshine.cs.uni-dortmund.de/~knoop/cocv02.html
This two-day workshop will bring together researchers in formal methods for hardware design and verification from academia and industry. It will allow participants to learn about the current state of the art in formally-based hardware verification and it is intended to spark debate about how more effective verification methods can be developed. Much research in hardware verification now takes place in industry, rather than in academia. For the long term survival of our field, we must ensure that academics and industrial researchers continue to work together on the real problems facing microprocessor developers and those developing System on a Chip solutions. A major aim of this workshop is to open the necessary communication channels. In addition to the submitted papers, there will be invited presentations by leading researchers in the field.
Contact: Mary Sheeran, Chalmers University of Technology and Prover Technology AB, Sweden
E-mail: ms@cs.chalmers.se
Web page: http://www.cs.chalmers.se/~ms/DCC02
The increasing decentralization and the growing share of software in technical systems require software systems development methods that guarantee correct, safe, and flexibly adjustable software. These have to incooperate a variety of modelling and description techniques, including techniques from engineering sciences, that have to be integrated. That means, methods and techniques have to be provided to compare different specifications, to establish semantic correspondences, to check their consistency, and to define the integrated semantics of collections of specifications.
The aim of the Workshop is to bring together Engineers and Computer Scientists to discuss such integration methods and approaches. Workshop topics include: integration of software modelling techniques and description techniques used in engineering; verification and model checking of combinations of specifications; general approaches to the integration of models and languages; case studies of integrated specifications for traffic control systems, production automation, or related areas.
Contact: Martin Große-Rhode, TU Berlin, Germany
E-mail: mgr@cs.tu-berlin.de
Web page: http://tfs.cs.tu-berlin.de/~mgr/int02
The aim of this one day workshop is to bring together researchers from academia and industry interested in the formal definition of languages, and in the use of the definitions for the derivation of tools and software applications such as: interactive transformation tools, software renovation tools, application generators, applications of formal methods to web technologies (XML, XSLT), etc. The workshop welcomes contributions based on all kinds and styles of formal language definition including attribute grammars, algebraic approaches, action semantics, operational semantics, and denotational semantics. Many aspects of the definition of languages, and the derivation of tools and applications are independent of the actual formalism used. The workshop also welcomes contributions to compare formalisms or to discuss the benefits and drawbacks of specific formalisms.
Contact: Marjan Mernik, University of Maribor, Slovenia
E-mail: marjan.mernik@uni-mb.si
Web page: http://www.cwi.nl/conferences/LDTA2002
Component-based approaches attract increasing attention of both research and industry. The rational behind this trend is in the promise of reuse. This is the idea to produce software by "plug & play" components which already exist or are produced by different external vendors. Components and software composition are considered to be a new way to overcome the remaining problems (e.g. reusability, deal with complexity) still not solved by the object-oriented paradigm.
In this context, the intention of this workshop is to collect different approaches and experiences. The gap between promise and reality is to be explored. The goal is to demystify these new approaches based on components and instead elaborate the real advantages, problems and challenges.
Contact: Elke Pulvermueller, University of Karlsruhe, Germany
E-mail: pulvermueller@acm.org
Web page: http://www.easycomp.org/sc2002
Engineering design languages are at the heart of today's tools employed for developing embedded systems. Their thorough semantic underpinning is a necessity to make them scale up with the ever increasing complexity of real-world systems and to interface them to state-of-the-art techniques for simulation, validation, and code generation. Recent years have seen growing interest in this field, with academic and industrial experts in concurrency theory, tool development, and formal validation techniques joining forces.
The workshop will provide an opportunity for this community to present novel and ongoing research, to demonstrate tools, and to discuss emerging ideas. Topics of interest include but are not limited to:
Contact: Gerald Luettgen, University of Sheffield, UK
E-mail: g.luettgen@dcs.shef.ac.uk
Web page: http://www.dcs.shef.ac.uk/~sfedl
Synchronous languages have been introduced in the 80s to program reactive systems. Such systems are characterized by their continuous reaction to their environment, at a speed determined by the latter. Synchronous languages have recently seen a tremendous interest from leading companies developing automatic control software for critical applications. The key advantage is that the synchronous approach has a rigorous mathematical semantics which allows the programmers to develop critical software faster and better.
SLAP 2002 is the first workshop devoted entirely to synchronous languages, applications, and programming. Its purpose is to bring together researchers and practitioners who work in the field of reactive systems. The workshop topics are covering all these issues: synchronous model of computation, synchronous languages and programming formalisms, compiling techniques, formal verification, test and validation of programs, case-studies...
Contact: Florence Maraninchi, INPG/Verimag, France
E-mail: florence.maraninchi@imag.fr
Web page: http://www.inrialpes.fr/bip/people/girault/Slap02
The SPIN workshop is a forum for researchers interested in the broad subject of model-checking technologies for analysis and verification of asynchronous, concurrent and distributed systems. Success in using these technologies to check properties of complex hardware and software systems has spurred a renewed interest in program verification in the broader software engineering communities. The ties between software engineering and model checking research are quite strong. We would like to continue to build the relationship between these research areas and encourage cross fertilization of ideas.
Contact: Stefan Leue, University of Freiburg, Germany
E-mail: spin2002@informatik.uni-freiburg.de
Web page: http://tele.informatik.uni-freiburg.de/spin2002
The study of time-dependent behavior is treated currently under different titles by different communities. Classical problems of manufacturing scheduling, for example, are considered as part of operation research and industrial engineering. Similar but different scheduling problems are encountered in the research on real-time operating systems. People who are interested in semantics, verification, or performance analysis are working on models such as timed automata, timed Petri nets, or max-plus algebra. Electrical engineers have to consider propagation delays in their circuits and designer of embedded controllers have to take into account the time it takes for the controller to compute its reaction after sampling the environment. The unifying theme underlying all these apparently different domains is that they treat systems whose behavior depends upon combinations of logical and temporal constraints, i.e., constraints on the distance between the occurrences of two events.
The workshop goal is to promote the study of fundamental and practical aspects of timed systems.
Contact: Oded Maler, CNRS/Verimag, France
E-mail: oded.maler@imag.fr
Web page: http://www-verimag.imag.fr/~maler/TPTS.html
Graphical specification formalisms exhibit an increasing popularity in the area of formal methods and their industrial applications. The ITU standardized notation of message sequence charts (MSC), the prototype of scenario-based languages, is now widely used for designing telecommunication protocols. MSCs allow the description of partial views of a system by abstracting away certain aspects like variable values, message contents, or internal behavior of submodules. This makes them very suitable as a method of partial specification in the early design stages of a system. MSCs are typically used as positive ("sunny day") or negative ("rainy day") scenarios which are required for the system which is being developed.
The aim of the workshop is to gather a larger community of researchers interested in scenario-based languages such as MSCs and to outline new trends and problems in the field.
Contact: Anca Muscholl, LIAFA, University of Paris VII, France
E-mail: muscholl@liafa.jussieu.fr