Newsletter 75
October 8, 2001
*******************************************************************
* Past issues of the newsletter are available at
http://www.lfcs.informatics.ed.ac.uk/lics/newsletters/
* Instructions for submitting an announcement to the newsletter
can be found at
http://www.lfcs.informatics.ed.ac.uk/lics/newsletters/inst.html
*******************************************************************
TABLE OF CONTENTS
* 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
ACM SIGACT-SIGMOD-SIGART SYMPOSIUM ON PRINCIPLES OF DATABASE SYSTEMS (PODS'01)
Call for Papers
Madison, Wisconsin June 3-6, 2002
http://www-db.cs.wisc.edu/sigmodpods2002
* 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:
http://www-db.cs.wisc.edu/sigmodpods2002
* 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).
REWRITING TECHNIQUES AND APPLICATIONS (RTA 2002)
Call for Papers
July 22 - 24, 2002 in Copenhagen, Denmark,
as part of the Federated Logic Conference FLoC'02
http://www.lifl.fr/~tison/RTA02.html
* 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)
CONFERENCE ON AUTOMATED DEDUCTION (CADE-18)
Call for Papers
July 27 - 30, 2002 in Copenhagen, Denmark,
as part of the Federated Logic Conference FLoC'02
http://www.uni-koblenz.de/~cade-18/
* 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
solicited.
* 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)
CONFERENCE ON COMPUTER AIDED VERIFICATION (CAV 2002)
Call for Papers
July 27 - 31, 2002 in Copenhagen, Denmark,
as part of the Federated Logic Conference FLoC'02
http://floc02.diku.dk/CAV
* 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
implementation.
* 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).
EUROPEAN JOINT CONFERENCES ON THEORY AND PRACTICE IN SOFTWARE (ETAPS 2002)
Call for Papers, Tool Demos, and Tutorials
Grenoble, France, April 6-14, 2002
http://www-etaps.imag.fr/
* 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
http://www.csr.UVic.CA/cc2002/
ESOP 2002, European Symposium On Programming
FASE 2002, Fundamental Approaches to Software Engineering
http://www.cis.cs.tu-berlin.de/~fase2002/index_general.html
FOSSACS 2002 Foundations of Software Science and Computation Structures
http://www.brics.dk/fossacs02/
TACAS 2002, Tools and Algorithms for the Construction and Analysis of Systems
http://www.dcs.ed.ac.uk/tacas2002/
* Satellite Events
ACL2: Third Workshop on the ACL2 Theorem Prover and its Applications
http://www.cs.utexas.edu/users/moore/acl2/workshop-2002/
AGT: APPLIGRAPH Workshop on Applied Graph Transformation
http://www.informatik.uni-bremen.de/theorie/AGT2002
CMCS: Coalgebraic Methods in Computer Science
http://www.cs.indiana.edu/cmcs
COCV: Compiler Optimization Meets Compiler Verification
http://sunshine.cs.uni-dortmund.de/~knoop/cocv02.html
DCC: Designing Correct Circuits
http://www.cs.chalmers.se/~ms/DCC02/
INT: Second Workshop on Integration of Specification Techniques for
Applications in Engineering
http://tfs.cs.tu-berlin.de/~mgr/int02/
LDTA: Second Workshop on Language Descriptions, Tools and Applications
http://www.cwi.nl/conferences/LDTA2002/
SC: Software Composition
http://i44www.info.uni-karlsruhe.de/~pulvermu/workshops/SC2002
SFEDL: Semantic Foundations of Engineering Design Languages
http://www.dcs.shef.ac.uk/~sfedl
SLAP: Synchronous Languages, Applications, and Programming
http://www.inrialpes.fr/bip/people/girault/Publications/Slap02
SPIN: 9th International SPIN Workshop on Model Checking of Software
http://tele.informatik.uni-freiburg.de/spin2002
TPTS: Theory and Practice of Timed Systems
http://www-verimag.imag.fr/~maler/TPTS.html
VISS: Validation and Implementation of Scenario-based Specifications
http://www.liafa.jussieu.fr/~anca/VISS02.html
* 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, Saddek.Bensalem@imag.fr
* 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, etaps2002-demo@brics.dk
* 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 INTERNATIONAL CONFERENCE ON GRAPH TRANSFORMATION (ICGT 2002)
First announcement
Barcelona (Spain), October 7-12, 2002
http://www.lsi.upc.es/icgt2002
* 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,
etc.
* 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)
LOGIC-BASED PROGRAM SYNTHESIS: STATE-OF-THE-ART & FUTURE TRENDS
(AAAI 2002 SPRING SYMPOSIUM)
Call for Papers
March 25-27, 2002, Stanford University.
http://ase.arc.nasa.gov/aaai2002
* 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
(SRI),
BOOK ANNOUNCEMENT
Modal and Temporal Properties of Processes
Colin Stirling
Springer-Verlag, 2001
http://www.springer-ny.com/detail.tpl?cart=9980395911806252&ISBN=0387987177
* 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.
BOOK ANNOUNCEMENT
Computability and Complexity Theory
by Steven Homer and Alan L. Selman
Springer Verlag, 2001
http://www.cse.Buffalo.EDU/~selman/book/
* 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:
http://www.springer-ny.com/detail.tpl?ISBN=0387950559
BOOK ANNOUNCEMENT
Knowledge in Action
Logical Foundations for Specifying and Implementing Dynamical Systems
Raymond Reiter
MIT Press, 2001
http://mitpress.mit.edu/0262182181
* 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.
BOOK ANNOUNCEMENT
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:
http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-67989-8
RESEARCH POSITIONS IN EDINBURGH AND MUNICH
* 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 http://www.lfcs.ed.ac.uk/mrg.
* Closing date: 31 Oct 2001.
Back to the LICS web page.