Newsletter 75
October  8, 2001

* Past issues of the newsletter are available at
* Instructions for submitting an announcement to the newsletter
  can be found at

* Calls for Papers
  ACM Symposium on Principles of Database Systems(PODS'01)
  Rewriting Tecniques and Applications (RTA 2002)
  Conference on Automated Deduction (CADE-18)
  Conference on Computer Aided Verification (CAV 2002)
  European joint conferences on Theory And Practice in Software
    (ETAPS 2002)
  International Conference on Graph Transformations (ICGT 2002)
  Logic-Based Program Synthesis: State-of-the-Art & Future Trends
* Book Announcements
  Modal and temporal properties of processes by C. Stirling
  Computability and Complexity Theory by S. Homer and A.L. Selman
  Knowledge in Action - Logical Foundations for Specifying and
    Implementing Dynamical Systems by R. Reiter
  Automated Theorem Proving in Software Engineering by J.M. Schumann
* Position Announcement
  Research Positions in Edinburgh and Munich

  Call for Papers
  Madison, Wisconsin  June 3-6, 2002
* Theme. The symposium invites papers in the fundamental aspects of databases.
  Original research papers on the theory, design, specification, or
  implementation of databases are solicited. Papers emphasizing new
  topics or foundations of emerging areas are especially welcomed.
* All submissions  must be done electronically.
  Detailed instructions for submissions can be found by following the
  "PODS Call for Papers" link at the SIGMOD/PODS 2002 homepage:
* Submission deadlines :
  November 2, 2001  - Paper registration and short abstracts due.
  November 9, 2001  - Papers due.
* Program Committee: Walid Aref (Purdue University), Catriel Beeri
  (Hebrew University of Jerusalem), Nicole Bidoit (University of
  Bordeaux), Surajit Chaudhuri (Microsoft Research), Thomas Eiter
  (Technical University of Vienna), Ronald Fagin (IBM Almaden Research
  Center), Giuseppe De Giacomo (University of Rome "La Sapienza"),
  Stephane Grumbach (INRIA), Dimitris Gunopulos (UC Riverside),
  Phokion G. Kolaitis (UC Santa Cruz and IBM Almaden Research Center,
  PC-chair), Leonid Libkin (University of Toronto), Jeff Naughton
  (University of Wisconsin, Madison), Ken Ross (Columbia University),
  Dan Suciu (University of Washington), Thomas Schwentick (University
  of Marburg), Jeffrey D. Ullman (Stanford University).

  Call for Papers
  July 22 - 24, 2002 in Copenhagen, Denmark,
  as part of the Federated Logic Conference FLoC'02
* RTA 2002 solicits original papers on all aspects of rewriting,
  including applications, foundations, frameworks, implementations,
  semantics. There are four submission categories: 1. regular research
  papers describing new results, 2. papers describing the experience
  of applying rewriting techniques in other areas, 3. problem sets
  that provide realistic and interesting challenges in the field of
  rewriting, 4. system descriptions.
* Best Paper Award: A prize of 500 EUR will be given to the best
  paper as judged by the program committee.
* Important Dates:
  Submissions to reach the program chairperson: January 15,  2002
  Notification to authors: March 22, 2002
  Final (camera-ready) copy due: April 25, 2002.
* Program Committee:
  Andrea Corradini (University of Pisa) Daniel J. Dougherty (Wesleyan
  University) Jürgen Giesl (RWTH Aachen) Bernhard Gramlich (TU Wien)
  Thérèse Hardin (University of Paris VI) Christopher Lynch (Clarkson
  University, Postdam) Jerzy Marcinkowski (University of Wroclaw) Aart
  Middeldorp (University of Tsukuba ) Joachim Niehren (University of
  Saarland) Femke van Raamsdonk (Free University Amsterdam) Albert
  Rubio (University of Barcelona ) Sophie Tison (University of Lille)
  Ralf Treinen (University Paris-Sud)

  Call for Papers
  July 27 - 30, 2002 in Copenhagen, Denmark,
  as part of the Federated Logic Conference FLoC'02
* CADE is the major international forum at which research on all
  aspects of automated deduction is presented. CADE-18 invites
  submissions related to all aspects of automated deduction, including
  foundations, implementations, and applications. Original research
  papers and descriptions of working automated deduction systems are
* The conference will include contributed papers (regular or
  experimental), system presentations, and invited lectures. There are
  three categories of submissions: Regular papers, experimental
  papers, and system descriptions.
* Important dates
  Submission deadline: February 2, 2002
  Notification of acceptance: March 29, 2002
  Camera-ready copy due: May 10, 2002
* Programme committee: Juergen Avenhaus (U Kaiserslautern), Franz
  Baader (RWTH Aachen), Leo Bachmair (U at Stony Brook), David Basin
  (Freiburg U), Peter Baumgartner (U Koblenz), Christoph Benzmueller
  (Saarland U), Maria Paola Bonacina (U of Iowa), Alan Bundy
  (Edinburgh U), Li Dafa (Tsinghua U), Anatoli Degtyarev (Liverpool),
  Gilles Dowek (INRIA Rocquencourt), Maarten de Rijke (U Amsterdam),
  Harald Ganzinger (Max-Planck Institute), Xiao-Shan Gao (Institute of
  Systems Science Beijing), Fausto Giunchiglia (Trento U), Jean
  Goubault-Larrecq (ENS Cachan), Reiner Haehnle (Chalmers U), John
  Harrison (INTEL), Ryuzo Hasegawa (Kyushu U), Tom Henzinger (U
  Berkeley), Steffen Hoelldobler (TU Dresden), Andrew Ireland
  (Heriot-Watt U), Mateja Jamnik (U Birmingham), Deepak Kapur (U New
  Mexico), Claude Kirchner (LORIA), Christoph Kreitz (Cornell U), Kim
  Larsen (Aalborg University), Alexander Leitsch (TU Vienna), Maurizio
  Lenzerini (U Roma si Sapienza), Alexander Lyaletski (Kyiv National
  University), Christopher Lynch (Clarkson U), Zohar Manna (Stanford
  U), Ursula Martin (St.Andrews U), Fabio Massacci (Siena U), Bill
  McCune (Argonne National Lab), Tom Melham (Glasgow), Dale Miller
  (Pennsylvania State U), Ralf Moeller (U Hamburg), Paliath Narendran
  (U at Albany), Ilkka Niemela (TU Helsinki), Robert Nieuwenhuis (TU
  Catalonia), Tobias Nipkow (TU Munich), Andreas Nonnengart (DFKI),
  Leszek Pacholski (U Wroclaw), Lawrence C. Paulson (Cambridge U),
  Frank Pfenning (Carnegie-Mellon U), David Plaisted (U of North
  Carolina at Chapel Hill), David Pym (Queen Mary and Westfield
  College), Manfred Schmidt-Schauss (Frankfurt U), Peter H. Schmitt (U
  Karlsruhe), Carsten Schuermann (Yale U), Natarajan Shankar (SRI
  International), John K. Slaney (Australian National U), Wayne Snyder
  (Boston U), Geoff Sutcliffe (U of Miami), Moshe Vardi (Rice U),
  Andrei Voronkov (U Manchester) (chair), Toby Walsh (York U), Igor
  Walukiewicz (U Warsaw), Christoph Weidenbach (Opel), Volker
  Weispfenning (U Passau)

  Call for Papers
  July 27 - 31, 2002 in Copenhagen, Denmark,
  as part of the Federated Logic Conference FLoC'02
* CAV'02 conference is the fourteenth in a series dedicated to the
  advancement of the theory and practice of computer-assisted formal
  analysis methods for software and hardware systems. The conference
  covers the spectrum from theoretical results to concrete
  applications, with an emphasis on practical verification tools and
  the algorithms and techniques that are needed for their
* The conference will include contributed papers, tool presentations,
  and invited lectures.  There are two categories of submissions:
  Regular  papers and tool presentations.
* Important Dates
  Paper submission: January 15, 2002
  Notification of acceptance: March 28, 2002
  Final version due: April 30, 2002
* Program Committee: David Basin (Freiburg), Armin Biere (Zürich),
  Thomas Ball (Microsoft), Ed Brinksma (Twente, co-chair), Werner Damm
  (Oldenburg), E. Allen Emerson (U. Texas-Austin), Alain Finkel (LSV),
  Nicolas Halbwachs (Verimag), Klaus Havelund (NASA), John Hatcliff
  (Kansas State Univ.), Thomas Henzinger (Stanford), Andreas Kuehlmann
  (Cadence), Orna Kupferman (Jerusalem), Kim Larsen (Aalborg,
  co-chair), Tim Leonard (Compaq), Ken McMillan (Cadence), Kedar
  Namjoshi (Bell Labs), Doron Peled (Bell Labs), Amir Pnueli
  (Weizmann), Natarajan Shankar (SRI), Joseph Sifakis (Verimag),
  Bernhard Steffen (Dortmund), Fabio Somenzi (U. Colorado), Wang Yi
  (Uppsala Univ.), Yaron Wolfsthal (IBM).

  Call for Papers, Tool Demos, and Tutorials
  Grenoble, France, April 6-14, 2002
* The European Joint Conferences on Theory and Practice of Software
  ETAPS is a loose and open confederation of conferences and other
  events that has become the primary European forum for academic and
  industrial researchers working on topics relating to Software Science.
* Important Dates:
  October 19, 2001:  Submissions Deadline for the Main Conferences,
                     Demos and Tutorials
  December 14, 2001: Notification of Acceptance/Rejection
  January 18 2002:   Camera-ready Version Due
  April 8-12, 2002:  ETAPS main Conferences in GRENOBLE
  April 6-14, 2001:  Satellite Events (different submission deadlines)
* Conferences
  CC 2002: International Conference on Compiler Construction
  ESOP 2002, European Symposium On Programming
  FASE 2002, Fundamental Approaches to Software Engineering
  FOSSACS 2002 Foundations of Software Science and Computation Structures
  TACAS 2002, Tools and Algorithms for the Construction and Analysis of Systems
* Satellite Events
  ACL2: Third Workshop on the ACL2 Theorem Prover and its Applications
  AGT: APPLIGRAPH Workshop on Applied Graph Transformation
  CMCS: Coalgebraic Methods in Computer Science
  COCV: Compiler Optimization Meets Compiler Verification
  DCC: Designing Correct Circuits
  INT: Second Workshop on Integration of Specification Techniques for
     Applications in Engineering
  LDTA: Second Workshop on Language Descriptions, Tools and Applications
  SC: Software Composition
  SFEDL: Semantic Foundations of Engineering Design Languages
  SLAP: Synchronous Languages, Applications, and Programming
  SPIN: 9th International SPIN Workshop on Model Checking of Software
  TPTS: Theory and Practice of Timed Systems
  VISS: Validation and Implementation of Scenario-based Specifications
* Tutorials. Proposals for half-day or full-day tutorials related to
  ETAPS 2001 are invited. Tutorial proposals will be evaluated on the
  basis of their assessed benefit for prospective participants to
  ETAPS 2001. Contact: Saddek Bensalem, Verimag,
* Tool Demonstrations. Demonstrations of tools presenting advances on
  the state of the art are invited. Submissions in this category
  should present tools having a clear connection to one of the main
  ETAPS conferences, possibly complementing a paper submitted
  separately. Contact: Peter D. Mosses,
* Invited Speakers. Ed Clarke, Carnegy Mellon University, USA (Spin
  workshop) Bruno Courcelle, LaBRI, Bordeaux, France Patrick Cousot,
  ENS Paris, France John Daniels, Syntropy Limited, London, UK Daniel
  Jackson, Massachusetts Institute of Technology, USA Michael Lowry,
  NASA Ames Research Center, USA Greg Morrisett, Cornell University,
  USA Mary Shaw, Carnegy Mellon University, USA

  First announcement
  Barcelona (Spain), October 7-12, 2002
* Theme. The field of Graph Transformation is concerned with the
  theory, applications and implementation issues of all formalisms for
  the modelling of the evolution of systems via any kind of
  transformation of graphical structures. Topics of interest include
  general models of graph transformation, node-, edge-, and hyperedge
  replacement, concurrency, distribution, term graph rewriting, graph
  decomposition, hierarchical graphs, parsing of graph languages,
  logic expression of graph transformation properties, analysis of
  graph transformation systems, structuring and modularization
  concepts, semantics of UML and other visual modelling techniques,
* Details of submissions to the main conference and the satellite
  workshops can be found on the ICGT 2002 website.
* Submission Deadline :  April 1, 2002.
* Program committee.  Michel Bauderon (Bordeaux, France), Paolo
  Bottoni (Rome, Italy), Andrea Corradini (co-chair; Pisa, Italy),
  Hartmut Ehrig (Berlin, Germany), Gregor Engels (Paderborn, Germany),
  Reiko Heckel (Paderborn, Germany), Dirk Janssens (Antwerp, Belgium),
  Hans-Jörg Kreowski (co-chair; Bremen, Germany), Ugo Montanari (Pisa,
  Italy), Manfred Nagl (Aachen, Germany), Fernando Orejas (Barcelona,
  Spain), Francesco Parisi-Presicce (Rome, Italy), Mauro Pezzé
  (Milano, Italy), John Pfaltz (Charlottesville, Virginia, USA), Rinus
  Plasmeijer (Nijmegen, The Netherlands), Detlef Plump (York, Great
  Britain), Azriel Rosenfeld (Maryland, USA), Grzegorz Rozenberg
  (Leiden, The Netherlands), Andy Schurr (Munich, Germany), Gabriele
  Taentzer (Berlin, Germany), Gabriel Valiente (Barcelona, Spain)

  Call for Papers
  March 25-27, 2002, Stanford University.
* Presentation.  "Automatic Programming" has long been considered a
  core AI task. C.  Green's and R. Waldinger's papers at the first
  IJCAI (1969) put it on a firm logical basis and spawned a long line
  of research. Some logic-based program synthesis systems have been
  developed and applied to different problem domains (e.g., Amphion,
  KIDS, Nuprl, Oyster/Clam). Yet, logic-based program synthesis is not
  a common approach to software development. Why not? The purpose of
  this symposium is to survey the current state of the art, to
  identify barriers, and to discuss directions which can help make it
  more feasible. We intend to go beyond the more calculus-oriented
  questions and try to cover a broad range of additional topics and
  questions, as for example representation of design knowledge, issues
  in constructive theorem-proving, issues in scaling up, role of
  synthesis in component-based approaches to system development,
  domains amenable for synthesis, support for certification, automatic
  program explanation
* Submissions. Potential participants should submit a position
  statement, extended abstract, or technical paper. Description of
  work in progress or recently completed work is very appropriate for
  the symposium; we especially solicit system descriptions.
* Important Dates
  Submission deadline:             October 5,  2001.
  Notification of acceptance:      November 9, 2001.
  Submission of accepted material: January 21, 2002.
* Organizing Committee B. Fischer (Co-Chair, RIACS/NASA Ames),
  D. Smith (Co-Chair, Kestrel Institute), D. Basin (U. Freiburg),
  A. Bundy (U. Edinburgh), Y. Deville (U. Louvain), P. Flener
  (U. Uppsala), C. Green (Kestrel Institute), C. Kreitz (Cornell),
  M. Lowry (NASA Ames), J. Richardson (Herriot-Watt), R. Waldinger

  Modal and Temporal Properties of Processes
  Colin Stirling
  Springer-Verlag, 2001
* Recently, temporal and modal logic, process calculi, and
  model checking have become essential software techniques for the
  formal verification of systems. Researchers and practitioners have
  found it useful to be able to express temporal properties of
  concurrent systems, especially liveness and safety properties. A
  safety property amounts to "nothing bad ever happens", whereas a
  liveness property expresses "something good does eventually
  happen". A logic expressing temporal notions provides a framework
  for the precise formalization of such specifications.
* In a clear and well-organized presentation, this book introduces
  concurrent processes as terms of an algebraic language comprising a
  few basic operators, whose behaviours are described using
  transitions. The book describes how families of such transitions can
  be arranged as labeled graphs - themselves concrete summaries of the
  behaviour of processes - and how various combinations of processes
  and their resulting behaviour are determined by transition rules. An
  extensive use of games for both equivalence and model checking
  provides an approach that is more conceptually clear than generally
  employed alternatives.

  Computability and Complexity Theory
  by Steven Homer and Alan L. Selman
  Springer Verlag, 2001
* This volume introduces materials that are the core knowledge in the
  theory of computation. The book is self-contained, with a
  preliminary chapter describing key mathematical concepts and
  notations and subsequent chapters moving from the qualitative
  aspects of classical computability theory to the quantitative
  aspects of complexity theory.  Dedicated chapters on undecidability,
  NP-completeness, and relative computability round off the work,
  which focuses on the limitations of computability and the
  distinctions between feasible and intractable.
* With its accessibility and well-devised organization, this
  text/reference is an excellent resource and guide for those looking
  to develop a solid grounding in the theory of computing. Beginning
  graduates, advanced undergraduates, and professionals involved in
  theoretical computer science, complexity theory, and computability
  will find the book an essential and practical learning tool.
* Publisher's Web Page:

  Knowledge in Action
  Logical Foundations for Specifying and Implementing Dynamical Systems
  Raymond Reiter
  MIT Press, 2001
* Modeling and implementing dynamical systems is a central problem in
  artificial intelligence, robotics, software agents, simulation,
  decision and control theory, and many other disciplines. In recent
  years, a new approach to representing such systems, grounded in
  mathematical logic, has been developed within the AI
  knowledge-representation community.
* This book presents a comprehensive treatment of these ideas, basing
  its theoretical and implementation foundations on the situation
  calculus, a dialect of first-order logic. Within this framework, it
  develops many features of dynamical systems modeling, including
  time, processes, concurrency, exogenous events, reactivity, sensing
  and knowledge, probabilistic uncertainty, and decision theory. It
  also describes and implements a new family of high-level programming
  languages suitable for writing control programs for dynamical
  systems. Finally, it includes situation calculus specifications for
  a wide range of examples drawn from cognitive robotics, planning,
  simulation, databases, and decision theory, together with all the
  implementation code for these examples. This code is available on
  the book's Web site.

  Automated Theorem Proving in Software Engineering
  Johann M. Schumann
  Foreword by Donald Loveland
  Springer Verlag, XIV+228 pp., 2001, ISBN 3-540-67989-8
* The growing demand for high quality, safety, and security of software
  systems can only be met by rigorous application of formal methods during
  software design. Tools for formal methods in general, however, do not
  provide a sufficient level of automatic processing. This book methodically
  investigates the potential of first-order logic automated theorem provers
  for applications in software engineering.
  Illustrated by complete case studies on verification of communication and
  security protocols and logic-based component reuse, the book characterizes
  proof tasks to allow an assessment of the prover's capabilities. Necessary
  techniques and extensions, e.g., for handling inductive and modal proof
  tasks, or for controlling the prover, are covered in detail.
  This book demonstrates that state-of-the-art automated theorem provers are
  capable of automatically handling important tasks during the development
  of high quality software and it provides many helpful techniques for
  increasing practical usability of the automated theorem prover for
  successful applications.
* Ordering info:

* Four research positions available, LFCS Edinburgh and LMU Munich, on
  "Mobile Resource Guarantees" project.  This is a collaborative
  project which is building foundational and practical infrastructure
  for endowing mobile code with independently verifiable certificates
  as to its resource consumption, in the form of condensed formal
  proofs, generated from typing derivations in linear type systems for
  describing resource bounds of high-level code.
* For information see
* Closing date: 31 Oct 2001.

Back to the LICS web page.