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, firstname.lastname@example.org, and Andrew J.I. Jones, email@example.com. * 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.