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, firstname.lastname@example.org * 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.