FOM: LICS newsletter

Stephen G Simpson simpson at
Thu Aug 9 11:49:25 EDT 2001

 From: Martin Grohe <grmail at>
 To: LICS List <grmail at>
 Subject: LICS Newsletter 74
 Date: Thu, 9 Aug 2001 15:54:37 +0100

 * 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,
   horty at, and Andrew J.I. Jones, ajijones at
 * 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 <Uwe.Nestmann at>
   Bjorn Victor <Bjorn.Victor at>

   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.

More information about the FOM mailing list