List of accepted papers

Invited lectures

Detecting bugs in Erlang programs using static analysis

Konstantinos Sagonas

This talk will review the main techniques used in the Dialyzer (Discrepancy AnaLYZer of ERlang programs) defect detection tool. Dialyzer employs various forms of static program analysis to automatically identify software errors in large applications written in Erlang, a concurrent functional language developed by Ericsson and commonly used for developing telecommunications software. Dialyzer is completely automatic, relatively fast, requires no annotations from its user to detect defects, and is exceptional in that it does not report any false positives. The heart of Dialyzer's analysis is inter-modular inference of success typings for Erlang functions and the talk will explain what success typings are and how they differ from type inference in statically typed languages.

alyzer, which nowadays is part of the Erlang/OTP (Open Telecom Platform) system, has been applied to large code bases of Erlang code and has identified a significant number of software defects that have remained unnoticed after years of extensive testing. The talk will also describe experiences and main lessons learned from Dialyzer's development and from feedback from its user community.

More information about the tool and a set of related publications can be found in Dialyzer's website.

Local Reasoning About Storable Locks

Josh Berdine

This talk will present a resource-oriented program logic that is able to reason about concurrent heap-manipulating programs with unbounded numbers of dynamically-allocated locks, and note an extension to storable threads. The logic is inspired by concurrent separation logic, but handles these more realistic concurrency primitives. We demonstrate that the proposed logic allows for local reasoning about programs that exhibit a high degree of information hiding in their locking mechanisms. Soundness is proved using a novel thread-local fixed-point semantics.

Regular Directional Types for Logic Programs

Witold Charatonik

Directional types assign each predicate in a logic program a pair of an input and an output type describing the possible argument terms before and after a call of the predicate. Regular types use tree automata for the effective representation of recursive data structures such as lists. In this talk, we discuss a type system for logic programs based on regular directional types.

Regular papers

Formalizing and Verifying Semantic Type Soundness of a Simple Compiler

Nick Benton and Uri Zarfaty

We describe a semantic type soundness result, formalized in the Coq proof assistant, for a compiler from a simple imperative language with heap-allocated data into an idealized assembly language. Types in the high-level language are interpreted as binary relations, built using both second-order quantification and a form of separation structure, over stores and code pointers in the low-level machine.

Interactive, Scalable, Declarative Program Analysis: From Prototype to Implementation

William C. Benton and Charles N. Fischer

Static analyses provide the semantic foundation for tools ranging from optimizing compilers to refactoring browsers and advanced debuggers. Unfortunately, developing new analysis specifications and implementations is often difficult and error-prone. Since analysis specifications are generally written in a declarative style, logic programming presents an attractive model for producing executable specifications of analyses. However, prior work on using logic programming for program analysis has focused exclusively on solving constraints derived from program texts by an external preprocessor. In this paper, we present DIMPLE, an analysis framework for Java bytecodes implemented in the Yap Prolog system. DIMPLE provides both a representation of Java bytecodes in a database of relations and a declarative domain-specific language for specifying new analyses as queries over this database. DIMPLE thus enables users to use logic programming for every step of the analysis development process, from specification to prototype to implementation. We demonstrate that our approach facilitates rapid prototyping of new program analyses and produces executable analysis implementations that are speed-competitive with specialized analysis toolkits.

User-definable Rule Priorities for CHR

Leslie De Koninck, Tom Schrijvers and Bart Demoen

This paper introduces CHR-rp: Constraint Handling Rules with user-definable rule priorities. CHR-rp offers flexible execution control which is lacking in CHR. A formal operational semantics for the extended language is given and is shown to be an instance of the theoretical operational semantics of CHR. It is discussed how the CHR-rp semantics influences confluence results. A translation scheme for CHR-rp programs with static rule priorities into (regular) CHR is presented. The translation is proven correct and benchmark results are given. CHR-rp is related to priority systems in other constraint programming and rule based languages.

Practical use of polynomials over the reals in proofs of termination

Salvador Lucas

Nowadays, polynomial interpretations are an essential ingredient in the development of tools for proving termination. Recently, we have proven that polynomial interpretations over the reals are strictly better for proving polynomial termination of rewriting than those which only use integer coefficients. Some essential aspects of their practical use, though, remain unexplored or underdeveloped. In this paper, we compare the two existing frameworks for using polynomial intepretations over the reals and show that one of them is strictly better than the other, thus making a suitable choice for implementations. We also prove that the use of algebraic real coefficients in the interpretations suffice for termination proofs. We also discuss the use of algorithms and techniques from Tarski's first-order logic of the real closed fields for implementing their use in proofs of termination. We argue that more standard constraint-solving techniques are better suited for this. We propose an algorithm to solve the polynomial constraints which arise when specific finite subsets of rational (or even algebraic real) numbers are considered for giving value to the coefficients. We provide a preliminary experimental evaluation of the algorithm which has been implemented as part of the termination tool MU-TERM.

Type Safe Dynamic Linking for JVM Access Control

Christian Skalka

The Java JDK security model provides an access control mechanism for the JVM based on dynamic stack inspection. Previous results have shown how stack inspection can be enforced at compile time via whole-program type analysis, but features of the JVM present significant remaining technical challenges. For instance, dynamic dispatch at the bytecode level requires special consideration to ensure flexibility in typing. Even more problematic is dynamic class loading and linking, which disallow a purely static analysis in principle, though the intended applications of the JDK exploit these features. We propose an extension to existing bytecode verification, that enforces stack inspection at link time, without imposing new restrictions on the JVM class loading and linking mechanism. Our solution is more flexible than existing type based approaches, and establishes a formal type safety result for bytecode-level access control in the presence of dynamic class linking.

Systematic Generation of Glass-Box Test Cases for Functional Logic Programs

Sebastian Fischer and Herbert Kuchen

We employ the narrowing-based execution mechanism of the functional logic programming language Curry in order to automatically generate a system of test cases for glass-box testing of Curry programs.

The test cases for a given function are computed by narrowing a call to that function with initially uninstantiated arguments.

The generated test cases are produced w.r.t. a selected code-coverage criterion such as control-flow coverage. Besides an adaption of the notion of control-flow coverage to functional (logic) programming, we present a novel coverage criterion for this programming paradigm. A particular difficulty of the adaption is the handling of laziness.

Mechanized Metatheory Model-Checking

James Cheney and Alberto Momigliano

The problem of formalizing and proving metatheoretic properties of programming language calculi, type systems, operational semantics, and related formal systems has received considerable attention recently. However, the dual problem ofsearching for errors in such formalizations has received comparatively little attention. In this paper, we consider the problem of bounded model-checking for metatheoretic properties of formal systems specified using nominal logic. In contrast to current state of the art for metatheory verification, our approach is fully automatic, does not require expertise in theorem proving on the part of the user, and produces counterexamples in the common case that a flaw is detected. Two counterexample search strategies are considered, one employing negation-as-failure and the other based on negation elimination; we compare the two approaches from the point of view of semantic complexity, implementation overhead, and efficiency.

Relational Semantics for Effect-Based Program Transformations with Dynamic Allocation

Nick Benton, Andrew Kennedy, Lennart Beringer and Martin Hofmann

We give a denotational semantics to a region-based effect systemtracking reading, writing and allocation in a higher-order language with dynamically allocated integer references.

Effects are interpreted in terms of the preservation of certain binary relations on the store, parameterized by region-indexed partial bijections on locations.

The semantics validates a number of effect-dependent program equivalences and can thus serve as a foundation for effect-based compiler transformations.

Higher-Order Semantic Labelling for Inductive Datatype Systems

Makoto Hamana

We give a novel transformation for proving termination of higher-order rewrite systems in the format of Inductive Data Type Systems (IDTSs) by Blanqui, Jouannaud and Okada. The transformation called higher-order semantic labelling attaches algebraic semantics of the arguments to each function symbol. We systematically define the labelling and show that labelled systems give termination models in the framework of Fiore, Plotkin and Turi's binding algebras. As applications, we give simple proofs of termination of the explicit substitution system lambdaX and currying transformation via higher-order semantic labelling. Moreover, we prove new results of modularity of termination of IDTSs by introducing the notion of solid IDTSs. We prove termination is preserved under the disjoint union of:

1. an IDTS and a higher-order program scheme (HO-RPS),
2. β-reduction, a confluent first-order system and a HO-RPS,
3. an IDTS and β-reduction.

Debugging Parallel Functional Languages

Alberto de la Encina, Luis Llana, Fernando Rubio and Mercedes Hidalgo-Herrero

Due to the use of higher-order functions and laziness, debugging lazy functional programs is not a trivial task. Fortunately, several debuggers have appeared during the last years. However, the difficulty of the debugging process is increased when considering parallel extensions of lazy functional languages. Thus, it is necessary not only to develop practical debuggers, but also to provide a clear semantic environment to understand what the debuggers should do. In this paper we present a formal framework for debugging two different parallel extensions of the lazy functional language Haskell. In order to do that, we define an operational semantics model which allows us to deal with side-effects and parallelism. By doing so, we provide a formalization of a parallel debugger we have already implemented by extending the sequential debugger Hood.

Computing with Subspaces

Bernd Brassel and Sergio Antoy

We propose a new definition and use of a primitive, called getAllValues, for computing all the values of a non-deterministic expression in a functional logic program. Our proposal restricts the validity of the argument of getAllValues. This restriction ensures that essential language features, such as the call-time choice semantics, the independence of the order of evaluation, and the referential transparency of the language, are preserved when getAllValues is executed. Up to now, conflicts between these language features and primitives like getAllValues have been seen as one of the main problems for employing such primitives in functional logic languages.

Real-Time Rewriting Semantics of Orc

Musab AlTurki and José Meseguer

Orc is a language proposed by Jayadev Misra for orchestration of distributed services. Orc is very simple and elegant, based on a few basic constructs, and allows succinct and understandable programming of sophisticated applications. However, because of its real-time nature and the different priorities given to internal and external events in an Orc program, giving a formal operational semantics that captures the real-time behavior of Orc programs is nontrivial and poses some interesting challenges. In this paper we propose such a real-time operational Orc semantics, that captures the informal operational semantics given by Misra. This operational semantics is given as a rewrite theory in which the elapse of time is explicitly modeled. The priorities between internal and external events are also modeled in two alternative ways: (i) by a rewrite strategy; and (ii) by adding extra conditions to the semantic rules. Since rewriting logic has efficient implementations such as Maude, we also get, directly out of the semantic definitions, both an Orc interpreter and an LTL model checker for Orc programs.

A Larger Decidable Semiunification Problem

Brad Lushman and Gordon V. Cormack

We present a graph-theoretic framework in which to study instances of the semiunification problem (SUP), which is known to be undecidable, but has several known and important decidable subsets. One such subset, the _acyclic_ semiunification problem (ASUP), has proved useful in the study of polymorphic type inference. We present graph-theoretic criteria in our framework that exactly characterize the ASUP acyclicity constraint. We then use our framework to find a decidable subset of SUP (which we call R-ASUP), which has a more natural description than ASUP, and strictly contains it.

Putting Declarative Programming into the Web: Translating Curry to JavaScript

Michael Hanus

We propose a framework to construct web-oriented user interfaces in a high-level way by exploiting declarative programming techniques. Such user interfaces are intended to manipulate complex data in a type-safe way, i.e., it is ensured that only type-correct data is accepted by the interface, where types can be specified by standard types of a programming language as well as any computable predicate on the data. The interfaces are web-based, i.e., the data can be manipulated with standard web browsers without any specific requirements on the client side. However, if the client's browser has JavaScript enabled, one could also check the correctness of the data on the client side providing immediate feedback to the user and reducing network traffic. In order to release the application programmer from the tedious details to interact with JavaScript, we propose an approach where the programmer must only provide a declarative description of the requirements of the user interface from which the necessary JavaScript programs and HTML forms are automatically generated. This approach leads to a very concise and maintainable implementation of web-based user interfaces. We demonstrate an implementation of this concept in the declarative multi-paradigm language Curry where the integrated functional and logic features are exploited to enable the high level of abstraction proposed in this paper.

Induction for Positive Almost Sure Termination

Isabelle Gnaedig

In this paper, we propose an inductive approach to prove positive almost sure termination of probabilistic rewriting under the innermost strategy. We extend to the probabilistic case a technique we proposed for termination of usual rewriting under strategies. The induction principle consists in assuming that terms smaller than the starting terms for an induction ordering are positively almost surely terminating. The proof is developed in generating proof trees, modelizing rewriting trees, in alternatively applying abstraction steps, expressing the application of the induction hypothesis, and narrowing steps, simulating the possible rewriting steps after abstraction. This technique is fully automatable for rewrite systems on constants, very useful to modelize probabilistic protocols.

Unfolding in CHR

Paolo Tacchella, Maria Chiara Meo and Maurizio Gabbrielli

Program transformation is an appealing technique which allows to improve run-time efficiency, space-consumption and more generally to optimize a given program. Essentially it consists of a sequence of syntactic program manipulations which preserves some kind of semantic equivalence. One of the basic operations which is used by most program transformation systems is unfolding which consists in the replacement of a procedure call by its definition. While there is a large body of literature on transformation and unfolding of sequential programs, very few papers have addressed this issue for concurrent languages and, to the best of our knowledge, no one has considered unfolding of CHR programs.

This paper is a first attempt to define a correct unfolding system for CHR programs. We define an unfolding rule, show its correctness and discuss some conditions which can be used to delete an unfolded rule while preserving the program meaning.

Nonmonotonic Inductive Logic Programming by Instance Patterns

Chongbing Liu and Enrico Pontelli

In this paper, we present a new approach, called NM-ILP-IP, for inductive learning in the context of nonmonotonic logic frameworks.This approach is based on the notations of concept instances and instance patterns.When a strictly correct Horn theory cannot be induced, this approach induces a normal logic program, by specializing a previously learned overly-general theory. The advantages of this approach over others include:

1. it does not rely on existing ILP systems, and it avoids many of the effectiveness and efficiency drawbacks of ordinary ILP systems;
2. no theorem prover is needed during the learning process;
3. it introduces negation as failure (NAF) of existing predicates and introduces new abnormality predicates only when necessary, making the final theory more compact.

A simple rewrite notion for call-time choice semantics

Francisco Lopez-Fraguas, Juan Rodriguez-Hortala and Jaime Sanchez-Hernandez

Non-confluent and non-terminating rewrite systems are interesting from the point of view of programming. In particular, existing functional logic languages use such kind of rewrite systems to define possibly non-strict non-deterministic functions. The semantics adopted for non-determinism is call-time choice, whose combination with non-strictness is not a trivial issue that has been addressed from a semantic point of view in the Constructor-based Rewriting Logic (CRWL) framework. We investigate here how to express call-time choice and non-strict semantics from a point of view closer to classical rewriting. The proposed notion of rewriting uses an explicit representation for sharing with let-constructions and is proved to be equivalent to the CRWL approach.

Efficient Trust Management Policy Analysis from Rules

Katia Hristova, K. Tuncay Tekle and Yanhong A. Liu

This paper describes a systematic method for deriving efficient algorithms and precise time complexities from extended Datalog rules as it is applied to the analysis of trust management policies specified in SPKI/SDSI, a well-known trust management framework designed to facilitate the development of secure and scalable distributed computing systems. The approach of expressing policy analysis problems as extended Datalog rules is much simpler than previous techniques for analysis of SPKI/SDSI policies. Our method also derives better, more precise time complexities than before in addition to generating complete algorithms and data structures. The method is general, with many applications beyond policy analysis. It extends our previous method for Datalog to handle list constructors, external functions, and queries.

Feasible reactivity in a synchronous π-calculus

Roberto Amadio and Frederic Dabrowski

Reactivity is an essential property of a synchronous program. Informally, it guarantees that at each instant the program fed with an input will “react” producing an output. In the present work, we consider a refined property that we call feasible reactivity. Beyond reactivity, this property guarantees that at each instant both the size of the program and its reaction time are bounded by a polynomial in the size of the parameters at the beginning of the computation and the size of the largest input. We propose a method to annotate programs and we develop related static analysis techniques that guarantee feasible reactivity for programs expressed in the S-π-calculus. The latter is a synchronous version of the π-calculus based on the SL synchronous programming model.