Newsletter 74
August 9, 2001
*******************************************************************
* The NEW URL of the LICS Webpages is
http://www.lfcs.informatics.ed.ac.uk/lics
*******************************************************************
* 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
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)
SIXTH INTERNATIONAL WORKSHOP ON DEONTIC LOGIC IN COMPUTER SCIENCE (DEON'02)
Call for Papers
Imperial College, London, UK, January 16-18, 2002
http://www.doc.ic.ac.uk/deon02
* 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@umiacs.umd.edu, and Andrew J.I. Jones, ajijones@dcs.kcl.ac.uk.
* 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).
FOURTH INTERNATIONAL SYMPOSIUM ON PRACTICAL ASPECTS OF DECLARATIVE
LANGUAGES (PADL'02)
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
BOOK ANNOUNCEMENT
Software Reliability Methods
Doron Peled
Springer-Verlag
http://www.springer.de/cgi-bin/search_book.pl?isbn=0-387-95106-7
* 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
engineering.
* 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
tools.
BOOK ANNOUNCEMENT
Java and the Java Virtual Machine - Definition, Verification, Validation
R. Staerk, J. Schmid, E. Boerger
Springer-Verlag, June 2001
http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-42088-6
* 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 http://www.inf.ethz.ch/~jbook/
BOOK ANNOUNCEMENT
The Logic of Knowledge Bases
Hector J. Levesque and Gerhard Lakemeyer
MIT Press
http://mitpress.mit.edu/promotions/books/LEVLHF00
* 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.
BOOK ANNOUNCEMENT
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
http://www.springer.de/cgi-bin/search_book.pl?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.
NEW JOURNAL
Theory and Practice of Logic Programming (TPLP)
Published bi-monthly as of January 2001
Cambridge University Press
http://uk.cambridge.org/journals/tlp/
* 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),
http://www.cwi.nl/projects/alp, the only organization representing
the interests of the logic programming community worldwide, endorsed
TPLP as its only journal.
SPECIAL ISSUE ON THE PI-CALCULUS
Call for Papers
Journal of Logic and Algebraic Programming
Special issue on the pi-Calculus
http://www.docs.uu.se/jlap01/
* NEW deadline for submissions: September 30, 2001
* Guest editors:
Uwe Nestmann
Bjorn Victor
LECTURERSHIP IN SEMANTICS OR AUTOMATED VERIFICATION
Division of Informatics
University of Edinburgh
http://www.jobs.ed.ac.uk/jobs/index.cfm?action=jobdet&jobid=245
* 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
http://www.informatics.ed.ac.uk 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
Edinburgh.
* 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
regarded.
* This post is available for 5 years.
Back to the LICS web page.