Programme

Seventh International Workshop on Constraint Handling Rules

Highlights

Outline

This page contains an general overview of invited talks, accepted papers and additional demo's, some screenshots and a demo video of the various tutorials and demo's, and a schedule for the worshop. A more detailed schedule is found on the FLoC website (also available with abstracts and side by side with other events).

The proceedings of the workshop is published as a technical report. Individual PDF versions of all accepted papers are available below or in the CHR Bibliography.

Invited Talks

Drools Business Logic integration Platform (Mark Proctor from JBoss). [Toggle abstract]
Abstract

Mark Proctor lead of the thriving, innovating JBoss Drools project. He will introduce the “Drools Business Logic integration Platform”, a fully featured business rule engine and management system that seamlessly integrates powerful Complex Event Processing and workflow capabilities.

More information on Drools and its four sub-projects—Guvnor (BRMS/BPMS), Expert (rule engine), Flow (process/workflow), and Fusion (event processing/temporal reasoning)—can be found at http://www.jboss.org/drools/
SWI Forms - Bringing logic to UI development (Matt Lilley from SecuritEase). [Toggle abstract]
Abstract

When developing rich, interactive, multi-user applications, a common task is creating interfaces to allow for user interaction. While there are many toolkits to achieve this using imperative languages, the task of translating use cases into imperative code can be time consuming, and is often difficult to analyze and check.
Over the past few years, SecuritEase has developed SWIF, or SWI-Forms, to tackle this problem in our Prolog-based application. By abstracting the UI elements from the logic describing their interactions, we separated form and function, allowing developers to focus on the two tasks independently. Further, by abstracting the logic itself into a series of high-level state transition rules, we remove the burden of managing the state directly, and reduce the specification of how user interactions affect the system to a purely logical form. This allows for rapid, but concise production of interfaces from use cases.
SWIF is an extensible, client-server based architecture, which will be released under the GPL. It includes a reference client implementation with an extensible set of UI widgets, a SWIF-based form creator, and an embeddable SWIF server, written in CHR/Prolog.
In this talk I will explain how SWIF enables the use of logic programming to vastly simplify the task of specifying user interface interactions.

Tutorials

Constraint Handling Rules (Thom Frühwirth) [Toggle abstract]
Abstract
In this tutorial, Thom Frühwirth, the creator of Constraint Handling Rules (CHR), will provide a broad introduction to the programming language. The tutorial is mainly aimed at newcomers to CHR, or to refresh your understanding of the language. The presentation covers a wide range of CHR related topics, ranging from theory to practice. This include language basics (syntax and formal semantics), a brief CHR programming guide, program analysis (e.g. confluence and termination), existing systems and implementations, and application.
CHRiSM — Chance Rules induce Statistical Models (Jon Sneyers) [Toggle abstract]
Abstract
CHRiSM is a new programming language, combining features of CHR and PRISM. It is a rule-based formalism for probabilistic-logic learning. In this brief introduction, we introduce the basic principles of the language. We introduce the syntax and the semantics, and illustrate the powerful capabilities of the language with examples. This presentation serves as an introduction to two other papers of this workshop: one on implementation aspects of CHRiSM, and one on an interesting application, namely automated music generation.

Accepted Papers

Application Papers

MTSeq – multi-touch-enabled music generation and manipulation based on CHR (Florian Geiselhart, Frank Raiser, Jon Sneyers and Thom Frühwirth). [Toggle abstract, PDF]
Abstract
We present MTSeq, an application that combines GUI-driven multi-touch input technology with the CHR-based music generation system APOPCALEAPS and an advanced audio engine. This combination leads to an extended user experience and an intuitive, playful access to the CHR music generation system, and thus introduces CHR to musicians and other non-computer-scientists in an appropriate way. The application is fully modularized and its parts are loosely interconnected through a standard IP networking layer, so it is optionally distributable across multiple machines.
Generic and Extensible Automatic Test Data Generation for Safety Critical Software with CHR (Ralf Gerlich from BSSE). [Toggle abstract, PDF]
Abstract

We present a new method for automatic test data generation (ATDG) applying to semantically annotated controlow graphs (CFGs), covering both ATDG based on source code and assembly or virtual machine code. The method supports a generic set of test coverage criteria, including all structural coverage criteria currently in use in industrial software test for safety critical software.

Several known and new strategies are supported for avoiding infeasible paths, that is paths in the CFG for which no input exists leading to their execution. We describe the implementation of the method in CHR^∨ and discuss divculties and advantages of CHR in this context.

About BSSE
BSSE has nearly 20 years of experience in automation of and in the software lifecycle, including automated and automatic software test based on random, heuristic and now constraint-based test data generation. BSSE testing tools have been applied on software of all criticality levels in projects for the European Space Agency (ESA) and the German Aerospace Center (DLR). BSSE also has experience in automotive, telecommunication and aviation applications.

Regular Papers

Result-directed CHR Execution (Jon Sneyers). [Toggle abstract, PDF]
Abstract
The traditional execution mode of CHR is bottom-up, that is, given a goal, the result is computed by exhaustively applying rules. This paper proposes a result-directed execution mode for CHR, to be used when both the goal and the result are known, and the task is to find all corresponding derivations. Result-directed execution is needed in the context of CHRiSM, a probabilistic extension of CHR in which goals typically have a large number of possible results. The performance of result-directed execution is greatly improved by adding early-fail rules.
Join Ordering for Constraint Handling Rules: Putting Theory into Practice (Peter Van Weert). [Toggle abstract, PDF]
Abstract
Join ordering is the NP-complete problem of finding the optimal order in which the different conjuncts of multi-headed rules are joined. Join orders are the single most important determinants for the runtime complexity of CHR programs. Nevertheless, all current systems use ad-hoc join ordering heuristics, often using greedy, very error-prone algorithms. As a first step, Leslie De Koninck and Jon Sneyers therefore worked out a more realistic, flexible formal cost model. In this work-in-progress paper, we show how we created a first practical implementation of static join ordering based on their theoretical model.
The Viterbi Algorithm expressed in Constraint Handling Rules (Henning Christiansen, Christian Theil Have, Ole Torp Lassen and Matthieu Petit). [Toggle abstract, PDF]
Abstract
The Viterbi algorithm is a classical example of a dynamic programming algorithm, in which pruning reduces the search space drastically, so that a potentially exponential time complexity is reduced to linearity. The central steps of the algorithm, expansion and pruning, can be expressed in a concise and clear way in CHR, but additional control needs to be added in order to obtain the desired time complexity. It is shown how auxiliary constraints, called trigger constraints, can be applied to fine-tune the order of CHR rule applications in order to reach this goal. It is indicated how properties such as confluence can be useful for showing such optimized programs correct.

System/tool Papers

A State Equivalence and Confluence Checker for CHRs (Johannes Langbein, Frank Raiser and Thom Frühwirth). [Toggle abstract, PDF]
Abstract
Analyzing confluence of CHR programs manually can be an impractical and time consuming task. Based on a new theorem for state equivalence, this work presents the first tool for testing equivalence of CHR states. As state equivalence is an essential component of confluence analysis, we apply this tool in the development of a confluence checker that overcomes limitations of existing checkers. We further provide evaluation results for both tools and detail their modular design, which allows for extensions and reuse in future implementations of CHR tools.

Demo

Long-term routing for autonomous sail boats with CHR (Ayman Adel Abdelsamie Abdelaal, Frank Raiser, Thom Frühwirth, and Roland Stelzer) [Toggle abstract]
Abstract
In this demo, we present a second work-in-progress application that combines GUI-driven multi-touch input technology and reasoning with Constraint Handling Rules (see also the application paper on MTSeq). It provides a rotatable and zoomable presentation of the earth. It is extended with forecast data for wind strengths, which an algorithm in CHR processes to offer route computations. The application is developed in cooperation with the Roboat project and aims to perform long-term routing for fully autonomous sailing boats.