ICLP on Friday, August 18th

Session 3: Invited Tutorial (09:00‑10:00)
Chair: Andrei Voronkov

09:00‑10:00

Brigitte Pientka (McGill University) Overcoming performance barriers: efficient verification techniques for logical frameworks [pdf] In recent years, logical frameworks which support formalizing language specifications together with their meta-theory have been pervasively used in small and large-scale applications, from certifying code [2] to advocating a general infrastructure for formalizing the meta-theory and semantics of programming languages [5]. In particular, the logical framework LF [9], based on the dependently typed lambda-calculus, and light-weight variants of it like LFi [17] have played a major role in these applications. While the acceptance of logical framework technology has grown and they have matured, one of the most criticized points is concerned with the run-time performance. In this tutorial we give a brief introduction to logical frameworks, describe its state-of-the art and present recent advances in addressing some of the existing performance issues.

Break (10:00‑10:30)

Session 4: Program Analysis (10:30‑12:30)
Chair: Harald Sondergaard

10:30‑11:00	Andy King (University of Kent) Lunjin Lu (Oakland University) Samir Genaim (UPM) Detecting Determinacy in Prolog Programs In program development it is useful to known that a call to a Prolog program will not inadvertently leave a choice-point on the stack. Determinacy inference has been proposed for solving this problem yet the analysis was found to be wanting in that it could not infer determinacy conditions for programs that contained cuts or applied certain tests to select a clause. This paper shows how to remedy these serious deficiencies. It also addresses the problem of identifying those predicates which can be rewritten in a more deterministic fashion. To this end, a radically new form of determinacy inference is introduced, which is founded on ideas in ccp, that is capable of reasoning about the way bindings imposed by a rightmost goal can make a leftmost goal deterministic.
11:00‑11:30	Xuan Li (Oakland University) Andy King (University of Kent) Lunjin Lu (Oakland University) Collapsing Closures A description in the sharing domain of Jacobs and Langen is a set of sharing groups where each sharing group is a subset of the set of program variables. The presence of a sharing group in a description indicates that all the variables in the group can be bound to terms that contain a common variable. The expressiveness of the domain, alas, is hampered by its intractability. Not only are descriptions potentially exponential in size, but abstract unification is formulated in terms of an operation, called closure under union, that is also exponential. This paper shows how abstract unification can be reformulated so that closure calculations can be collapsed in two senses. Firstly, one closure operation can be folded into another so as to reduce the total number of closures that need to be computed. Secondly, the remaining closures are applied to smaller descriptions so, although the operation remains exponential, the overhead of closure calculation is reduced.
11:30‑12:00	Elvira Albert (Complutense University of Madrid) Puri Arenas (Complutense University of Madrid) German Puebla (Technical University of Madrid) Manuel Hermenegildo (T.U. Madrid (UPM) and U. of New Mexico (UNM)) Reduced Certificates for Abstraction-Carrying Code Abstraction-Carrying Code (ACC) has recently been proposed as a framework for mobile code safety in which the code supplier provides a program together with an abstraction (or abstract model of the program) whose validity entails compliance with a predefined safety policy. The abstraction plays thus the role of safety certificate and its generation is carried out automatically by a fixed-point analyzer. The advantage of providing a (fixed-point) abstraction to the code consumer is that its validity is checked in a single pass (i.e., one iteration) of an abstract interpretation-based checker. A main challenge to make ACC useful in practice is to reduce the size of certificates as much as possible while at the same time not increasing checking time. The intuitive idea is to only include in the certificate information that the checker is unable to reproduce without iterating. We introduce the notion of reduced certificate which characterizes the subset of the abstraction which a checker needs in order to validate (and re-construct) the full certificate in a single pass. Based on this notion, we instrument a generic analysis algorithm with the necessary extensions in order to identify the information relevant to the checker. Then, we study what the effects of reduced certificates are on the correctness and completeness of the checking process. We provide a correct checking algorithm together with sufficient conditions for ensuring its completeness. Our approach has been implemented and benchmarked within the CiaoPP system. The experimental results show that our proposal is able to greatly reduce the size of certificates in practice.
12:00‑12:30	Alberto Pettorossi (DISP, University of Roma Tor Vergata, Roma (Italy)) Maurizio Proietti (IASI-CNR) Valerio Senni (DISP, University of Roma Tor Vergata, Roma (Italy)) Proving Properties of Constraint Logic Programs by Eliminating Existential Variables We consider a class of constraint logic programs which manipulate finite lists of real numbers. Constraints are linear equations and disequations over reals. We propose a method for proving first order properties of this class of programs. Our method consists in converting any given first order formula into a stratified constraint logic program and then applying a suitable unfold/fold transformation strategy that preserves the perfect model. The gist of our strategy is the elimination of existential variables, that is, variables which occur in the body of a clause and not in its head. Since, in general, the first order properties of the class of programs we consider are undecidable, our strategy is necessarily incomplete. However, the experiments we have made with a prototype implementation show that our method is powerful enough to prove many non-trivial program properties.

Lunch break (12:30‑14:00)

Session 5: Answer Set Programming (14:00‑16:00)
Chair: I.V. Ramakrishnan

14:00‑14:30	Enrico Pontelli (New Mexico State University) Tran Son (NMSU) Justifications for Logic Programs under Answer Set Semantics The paper introduces the notion of off-line justification for Answer Set Programming. Justifications provide a graph-based explanation of the truth value of an atom w.r.t. a given answer set. The notion of justification accounts for the specifics of answer set semantics. The paper extends also this notion to provide justification of atoms during the computation of an answer set (\emph{on-line justification}), and presents an integration of on-line justifications within the computation model of Smodels. Off-line and on-line justifications provide useful tools to enhance understanding of answer set programs, and they offer a basic data structure for the development of methodologies and tools for debugging answer set programs. A preliminary implementation has been developed in the ASP-Prolog system.
14:30‑15:00	Katsumi Inoue (National Institute of Informatics) Chiaki Sakama (Wakayama University) Generality Relations in Answer Set Programming This paper studies generality relations on logic programs. Intuitively, a program P_1 is more general than another program P_2 if P_1 gives us more information than P_2. In this paper, we define various kinds of generality relations over nonmonotonic programs in the context of answer set programming. The semantic properties of generality relations are investigated based on domain theory, and both a minimal upper bound and a maximal lower bound are constructed for any pair of logic programs. We also introduce the concept of strong generality between logic programs and investigate its relationships to strong equivalence. These results provide a basic theory to compare the degree of incompleteness between nonmonotonic logic programs, and also have important applications to inductive logic programming and multi-agent systems.
15:00‑15:30	Davy Van Nieuwenborgh (Vrije Universiteit Brussel) Stijn Heymans (DERI Innsbruck, University of Innsbruck) Dirk Vermeir (Vrije Universiteit Brussel) Cooperating Answer Set Programming We present a formalism for logic program cooperation based on the answer set semantics. The system consists of independent logic programs that are connected via a sequential communication channel. When presented with an input set of literals from its predecessor, a logic program computes its output as an answer set of itself, enriched with the input. It turns out that the communication strategy makes the system quite expressive: essentially a sequence of a fixed number of programs n captures the n-th level of the polynomial hierarchy. On the other hand, unbounded sequences capture the polynomial hierarchy. These results make the formalism suitable for complex applications such as hierarchical decision making and preference-based diagnosis on ordered theories. In addition, such systems can be realized by implementing an appropriate control strategy on top of existing solvers such as dlv or smodels, possibly in a distributed environment.
15:30‑16:00	Johan Wittocx (K.U. Leuven) Joost Vennekens (K.U. Leuven) Maarten Mariën (K.U. Leuven) Marc Denecker (K.U.Leuven) Maurice Bruynooghe (K.U. Leuven) Predicate Introduction under Stable and Well-founded Semantics This paper studies the tranformation of ``predicate introduction'': Replacing a complex formula in an existing logic program by a newly defined predicate. From a knowledge representation perspective, such transformations can be used to eliminate redundancy or to simplify a theory. From a more practical point of view, they can also be used to transform a theory into a normal form imposed by certain inference programs or theorems, e.g., by eliminating universal quantifiers. In this paper, we study when predicate introduction is equivalence preserving under the stable and well-founded semantics. We do this in the algebraic framework of ``approximation theory''; this is a fixpoint theory for non-monotone operators that generalizes all main semantics of various non-monotone logics, including Logic Programming, Default Logic and Autoepistemic Logic. We prove an abstract, algebraic equivalence result and then instantiate this abstract theorem to Logic Programming under the stable and well-founded semantics.

Break (16:00‑16:30)

Invited Talk (16:30‑17:30)
Chair: Sandro Etalle

16:30‑17:30

Monica Lam (Stanford University) Why Use Datalog to Analyze Programs? [ppt] We use Datalog because (1) we can write program analyses easier and (2) the analyses in Datalog run faster! As we turn to automatic program analysis to improve software reliability and security, we find it necessary to perform more complex program analyses. Specifically, if we wish to reason about heap objects, we must perform an interprocedural pointer alias analysis that distinguishes between calling contexts. This is challenging because a typical large program can have over 10^14 calling contexts, even if we collapse all recursive cycles. We discovered that it is possible to represent the exponentially many context-sensitive points-to relations succinctly using binary decision diagrams (BDDs). However, it took us months to make just one analysis run at speed. We automated the optimization process and implemented a system called bddbddb (BDD-Based Deductive DataBase), which uses active machine learning to translate Datalog into efficient BDD operations. A pointer alias analysis now takes just tens of lines of Datalog code rather than thousands of lines of Java code. Pointer alias analysis by itself is not useful. So, more importantly, we can use the results of pointer alias analysis to compute the information of interest by writing a few more Datalog rules. For example, we have used this approach to find numerous vulnerabilities in large C and Java programs. The use of Datalog makes it possible for unsophisticated users to use complex context-sensitive analysis to answer some of the hard questions about their programs. The research discussed in the talk was performed jointly with John Whaley, Ben Livshits, Michael Martin, Dzintars Avots, Michael Carbin, and Christopher Unkel. It is supported in part by the National Science Foundation under Grant No. 0326227, NSF Graduate Student Fellowships, Stanford Graduate Fellowships, and an Intel student fellowship.

ICLP Banquet (19:00‑22:00)