Newsletter 74
August  9, 2001

* The NEW URL of the LICS Webpages is
* Past issues of the newsletter are available at
* Instructions for submitting an announcement to the newsletter
  can be found at

* Calls for Papers
  Workshop on Deontic Logic in Computer Science
  Symposium on Practical Aspects of Declarative Languages (PADL '02)
* Book Announcements
  Software Reliability Methods by D. Peled
  Java and the Java Virtual Machine - Definition, Verification,
    Validation by R. Staerk, J. Schmid, E. Boerger
  The Logic of Knowledge Bases by H.J. Levesque and G. Lakemeyer
  Systems and Software Verification. Model-Checking Techniques and
    Tools by B. Berard, M. Bidoit, A. Finkel, F. Laroussinie,
    A. Petit, L. Petrucci and Ph. Schnoebelen
* Journals
  Theory and Practice of Logic Programming
  Journal of Logic and Algebraic Programming Special Issue on Pi-Calculus
* Position Announcement
  Lecturership in Sematics or Automated Verification (Edinburgh)

  Call for Papers
  Imperial College, London, UK, January 16-18, 2002
* Theme. The logical study of normative reasoning, including formal systems of
  deontic logic, defeasible normative reasoning, the logic of action, and
  other areas of logic related to normative reasoning. The formal analysis of
  normative concepts and normative systems. The formal representation of legal
  knowledge. The formal specification of aspects of norm-governed multi-agent
  systems and autonomous agents. The formal specification of normative systems
  for the management of  bureaucratic processes in public or private
  administration. Applications of normative logic to the specification of
  databases and computer security protocols. Normative aspects of protocols
  for communication, negotiation and  multi-agent decision making.
* Submissions can be done electronically, by email to John Horty,, and Andrew J.I. Jones,
* Submission deadline: September 1, 2001
* Programme Committee.  John Horty (University of Maryland, co-chair), Andrew
  J.I. Jones (King's College, London, co-chair), Paul Bartha (University of
  British Columbia), Mark Brown (Syracuse University), Jose Carmo (University
  of Madeira), Laurence Cholvy (ONERA Toulouse), Frederic Cuppens (ONERA
  Toulouse), Robert Demolombe (ONERA Toulouse), Lou Goble (Willamette
  University), Risto Hilpinen (University of Maimi), Lars Lindahl (University
  of Lund), Paul McNamara (University of New Hampshire), David Makinson (UNESCO
  Paris), John-Jules Meyer (Utrecht University), Donald Nute (University of
  Georgia), Giovanni Sartor (University of Bologna), Krister Segerberg (Uppsala
  University), Marek Sergot (Imperial College, London), Leon van der Torre
  (Vrije Universiteit Amsterdam), Lennart Aqvist (Uppsala University).

  Call for Papers
  Portland, Oregon, USA
  Jan 19-20, 2002
* PADL provides a forum for researchers, practitioners, and
  implementors of declarative languages to exchange ideas on current
  and novel application areas and on the requirements for effective
  deployment of declarative systems.  We invite papers dealing with
  practical applications of newly discovered results and techniques in
  logic, constraint, and functional programming.  Papers dealing with
  practical applications of theoretical results, new techniques of
  implementation with considerable impact on an application, or
  innovative applications are particularly welcome.  Position papers
  as well as papers that present works in progress are also welcome.
* The scope of PADL includes, but is not limited to: Innovative
  applications of declarative languages, Declarative domain-specific
  languages and applications, New developments in declarative
  languages and their impact on applications o Practical experiences,
  Evaluation of implementation techniques on practical applications,
  Novel uses of declarative languages in the classroom
  The papers should highlight the practical contribution of the work
  and  the relevance of  declarative languages  to achieve that end.
* Important Dates:
  Paper Submission: Aug. 10, 2001
  Notification: Oct. 8, 2001
  Camera Ready: Nov. 5, 2001
  Symposium: Jan. 19-20, 2002
* Program Committee (still being constituted): Sergio Antoy, Gopal
  Gupta, Joxan Jaffar, Fergus Henderson, Shriram Krishnamurthi
  (co-chair), Andrew Kennedy, Michael Leuschel, Kim Marriott, John
  Peterson, Andreas Podelski, Enrico Pontelli, C.R. Ramakrishnan
  (co-chair), John Reppy, Manuel Serrano, Olin Shivers, Paul Tarau

  Software Reliability Methods
  Doron Peled
* The book 'Software Reliability Methods' presents a collection and
  comparison of current methods for dealing with software
  reliability. It compares between these methods, and shows their
  advantages and disadvantages. The book presents a description of the
  techniques, intended for a nonexpert audience with some minimal
  technical background (e.g., some training in software engineering,
  or basic computer science courses). It also describes some advanced
  techniques, aimed at researchers and practitioners in software
* This text/reference is intended to be used as an introduction to
  software methods techniques, a source for learning about various
  ways to enhanced software reliability, a reference on formal methods
  technique, and also as a basis for a one semester university course
  in this subject. It suggests various projects and exercises for
  achieving "hands-on" experience with the various formal methods

  Java and the Java Virtual Machine - Definition, Verification, Validation
  R. Staerk, J. Schmid, E. Boerger
  Springer-Verlag, June 2001
* This book provides a high-level description, together with a
  mathematical and an experimental analysis, of Java and of the Java
  Virtual Machine (JVM), including a standard compiler of Java
  programs to JVM code and the security critical bytecode verifier
  component of the JVM. The description is structured into language
  layers and machine components. It comes with a natural executable
  refinement (written in AsmGofer and provided on CD ROM) which can be
  used for testing code. The method developed for this purpose is
  based on Abstract State Machines (ASMs) and can be applied to other
  virtual machines and to other programming languages as well. The
  book is written for advanced students and for professionals and
  practitioners in research and development who need a complete and
  transparent definition and an executable model of the language and
  of the virtual machine underlying its intended implementation. The
  CD ROM contains the entire text of the book and numerous examples
  and exercises.
* The AsmGofer executable models and additional lecturing material can
  be downloaded from

  The Logic of Knowledge Bases
  Hector J. Levesque and Gerhard Lakemeyer
  MIT Press
* The idea of knowledge bases lies at the heart of symbolic, or
  "traditional," artificial intelligence. A knowledge-based system
  decides how to act by running formal reasoning procedures over a
  body of explicitly represented knowledge--a knowledge base. The
  system is not programmed for specific tasks; rather, it is told what
  it needs to know and expected to infer the rest.
* This book is about the logic of such knowledge bases. It describes
  in detail the relationship between symbolic representations of
  knowledge and abstract states of knowledge, exploring along the way
  the foundations of knowledge, knowledge bases, knowledge-based
  systems, and knowledge representation and reasoning. Assuming some
  familiarity with first-order predicate logic, the book offers a new
  mathematical model of knowledge that is general and expressive yet
  more workable in practice than previous models. The book presents a
  style of semantic argument and formal analysis that would be
  cumbersome or completely impractical with other approaches.  It also
  shows how to treat a knowledge base as an abstract data type,
  completely specified in an abstract way by the knowledge-level
  operations defined over it.

  Systems and Software Verification. Model-Checking Techniques and Tools.
  B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci and
  Ph. Schnoebelen
  Springer-Verlag, ISBN 3-540-41523-8
* Model checking is a powerful approach for the formal verification of
  software. When applicable, it automatically provides complete proofs of
  correctness, or explains, via counter-examples, why a system is not correct.
  This book provides a basic introduction to this new technique.  The first
  part describes in simple terms the theoretical basis of model checking:
  transition systems as a formal model of systems, temporal logic as a formal
  language for behavioral properties, and model-checking algorithms.  The
  second part explains how to write rich and structured temporal logic
  specifications in practice, while the third part surveys some of the major
  model checkers available.

  Theory and Practice of Logic Programming (TPLP)
  Published bi-monthly as of January 2001
  Cambridge University Press
* This journal was founded by the former editors of the Journal of
  Logic Programming (JLP) who in November 1999 collectively resigned
  to found TPLP. In the period from the JLP inception in 1984 until
  1999 its price per page increased by the staggering amount of 314%.
  The subscription price per page of TPLP for libraries is 60% cheaper
  than JLP.
* The Association for Logic Programming (ALP),, the only organization representing
  the interests of the logic programming community worldwide, endorsed
  TPLP as its only journal.

  Call for Papers
  Journal of Logic and Algebraic Programming
  Special issue on the pi-Calculus
* NEW deadline for submissions: September 30, 2001
* Guest editors:
  Uwe Nestmann 
  Bjorn Victor 

  Division of Informatics
  University of Edinburgh
* The Division of Informatics has a very strong tradition of research
  in computer systems, theoretical computer science, cognitive
  science, artificial intelligence, robotics and neural networks (see for details). Working within the Laboratory
  for Foundations of Computer Science, you will add to our existing
  strengths in research and teaching, integrate your own research with
  that of others and contribute to the development of Informatics at
* Your research interest in the general area of Semantics of
  Computation or in the application of automatic verification
  techniques to check properties of software, would be highly
* This post is available for 5 years.

Back to the LICS web page.