ICLP on Monday

Detailed program
Monday July 29th, 2002
See also the unified by-slot program


Sessions take place in auditorium 4 unless otherwise indicated.

Session 1: Introduction and Best Papers

Chair: Peter Stuckey and Henning Christiansen

09:15-09:30  Introduction and Prize Giving

09:30-10:00  Alessandra Russo, Imperial College, UK
Rob Miller, U College London, UK
Bashar Nuseibeh, The Open U, UK
Jeff Kramer, Imperial College, UK
An abductive approach for analysing event-based requirements specifications
We present a logic and logic programming based approach for analysing event-based requirements specifications given in terms of a system's reaction to events and safety properties. The approach uses a variant of Kowalski and Sergot's Event Calculus to represent such specifications declaratively and an abductive reasoning mechanism for analysing safety properties. Given a system description and a safety property, the abductive mechanism is able to identify a complete set of counterexamples (if any exist) of the property in terms of symbolic "current" states and associated event-based transitions. A case study of an automobile cruise control system specified in the SCR framework is used to illustrate our approach. The technique described is implemented using existing tools for abductive logic programming.

10:00-10:30  Tom Schrijvers, K.U. Leuven, Belgium
María García de la Banda, Monash U, Australia
Bart Demoen, K.U. Leuven, Belgium
Trailing analysis for HAL
The HAL language includes a Herbrand constraint solver which uses Taylor's PARMA scheme rather than the standard WAM representation. This allows HAL to generate more efficient Mercury code. Unfortunately, PARMA's variable representation requires value trailing with a trail stack consumption about twice as large as for the WAM. We present a trailing analysis aimed at determining which Herbrand variables do not need to be trailed. The accuracy of the analysis comes from HAL's semi-optional determinism and mode declarations. The analysis has been partially integrated in the HAL compiler and benchmark programs show good speed-up.

Session 2: Applications I

Chair: Ulf Nilsson

11:00-11:30  Steve Barker, U Westminster, UK
Access control for deductive databases by logic programming
We show how logic programs may be used to protect deductive databases from the unauthorized retrieval of positive and negative information, and from unauthorized insert and delete requests. To achieve this protection, a deductive database is expressed in a form that is guaranteed to permit only authorized access requests to be performed. The protection of the positive information that may be retrieved from a database and the information that may be inserted are treated in a uniform way as is the protection of the negative information in the database, and the information that may be deleted.

11:30-12:00  Kung-Kiu Lau, U Manchester, UK
Michel Vanden Bossche, Mission Critical, Belgium
Logic programming for software engineering: A second chance
Current trends in Software Engineering and developments in Logic Programming lead us to believe that there will be an opportunity for Logic Programming to make a breakthrough in Software Engineering. In this paper, we explain how this has arisen, and justify our belief with a real-life application. Above all, we invite fellow workers to take up the challenge that the opportunity offers.

12:00-12:30  Alexander Bockmayr, LORIA Nancy, France
Arnaud Courtois, LORIA Nancy, France
Using hybrid concurrent constraint programming to model dynamic biological systems
Systems biology is a new area in biology that aims at achieving a systems-level understanding of biological systems. While current genome projects provide a huge amount of data on genes or proteins, lots of research is still necessary to understand how the different parts of a biological system interact in order to perform complex biological functions. Computational models that help to analyze, explain or predict the behavior of biological systems play a crucial role in systems biology. The goal of this paper is to show that hybrid concurrent constraint programming (Gupta/Jagadeesan/Saraswat 98) may be a promising alternative to existing modeling approaches in systems biology. Hybrid cc is a declarative compositional programming language with a well-defined semantics. It allows one to model and simulate the dynamics of hybrid systems, which exhibit both discrete and continuous change. We show that Hybrid cc can be used naturally to model a variety of biological phenomena, such as reaching thresholds, kinetics, gene interaction or biological pathways.

Session 3: Invited Tutorial

14:00-15:30  David S. Warren, State U of New York-Stony Brook, USA
Invited tutorial: Tabled logic programming

Session 4: Tabling and Deductive Databases

Chair: Kostis Sagonas

16:00-16:30  Witold Charatonik, MPI Saarbrücken, Germany
Supratik Mukhopadhyay, MPI Saarbrücken, Germany
Andreas Podelski, MPI Saarbrücken, Germany
Constraint-based infinite model checking and tabulation for stratified CLP
We consider Gottlob, Grädel and Veith's translation of branching time logic into Datalog LITE where global model checking amounts to bottom-up query evaluation. We define the safe branching time logic Sµ that yields the fragment Datalog LIT under this translation, and investigate an alternative evaluation strategy for this fragment. Datalog LIT corresponds to Stratified CLP when we represent the transition relation of an infinite-state system by a CLP program. We give a tabulation procedure for the top-down evaluation of stratified CLP programs and thus obtain a constraint-based local model checking procedure for Sµ.

16:30-17:00  Giridhar Pemmasani, State U of New York-Stony Brook, USA
C. R. Ramakrishnan, State U of New York-Stony Brook, USA
I. V. Ramakrishnan, State U of New York-Stony Brook, USA
Efficient real-time model checking using tabled logic programming and constraints
Logic programming based tools for real-time model checking are beginning to emerge. In a previous work we had demonstrated the feasibility of building such a model checker by combining constraint processing and tabulation. But efficiency and practicality of such a model checker were not adequately addressed. In this paper we describe XMC/dbm, an efficient model checker for real-time systems using tabling. Performance gains in XMC/dbm directly arise from the use of a lightweight constraint solver combined with tabling. Specifically the timing constraints are represented by difference bound matrices which are encoded as Prolog terms. Operations on these matrices, the dominant component in real-time model checking, are shared using tabling. We provide experimental evidence that the performance of XMC/dbm is considerably better than our previous real-time model checker and is highly competitive to other well known real-time model checkers implemented in C/C++. An important aspect of XMC/dbm is that it can handle verification of systems consisting of untimed components with performance comparable to verification systems built specifically for untimed systems.

17:00-17:30  Hasan M. Jamil, Mississipi State U, USA
Gillian Dobbie, U Auckland, New Zealand
A model theoretic semantics for multi-level secure deductive databases
The impetus for our current research is the need to provide an adequate framework for belief reasoning in multi-level secure (MLS) databases. We demonstrate that a prudent application of the concept of inheritance in a deductive database setting will help capture the notion of declarative belief and belief reasoning in MLS databases in an elegant way. In this paper, we show that these concepts can be captured in a F-logic style declarative query language, called MultiLog, for MLS deductive databases for which a model theoretic semantics exists. This development is significant from a database perspective as it now enables us to compute the semantics of MultiLog databases in a bottom-up fashion. The semantics developed here is reminiscent of the stable model semantics of logic programs with negation. We also define a bottom-up procedure to compute unique models of stratified MultiLog databases. Finally, we also establish the equivalence of MultiLog's three logical characterizations - model theory, fixpoint theory and proof theory.

17:30-18:30  Poster session

Room: Lobby

18:40-19:00  ICLP Bus leaving to City Hall

Room: Main entrance

19:00-21:00  City Hall reception

Joint with CADE, CAV, TABLEAUX
Room: City Hall