CHR on Tuesday, July 20th

09:00‑10:00 Invited Talk
Location: AT 2.11
09:00 Mark Proctor (JBoss)
Drools Business Logic integration Platform Tutorial

In this tutorial, Mark Proctor, lead of the thriving, innovating JBoss Drools project, 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/

10:30‑12:30 Session 1 (highlights: CHR Tutorial & Invited Talk)
Location: AT 2.11
10:30 Thom Frühwirth (University of Ulm)
Constraint Handling Rules Tutorial

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.

11:15 Johannes Langbein, Frank Raiser and Thom Fruehwirth
A State Equivalence and Confluence Checker for CHR

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.

11:40 Peter Van Weert
Join Ordering for Constraint Handling Rules: Putting Theory into Practice

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.

12:05 Matt Lilley (SecuritEase)
SWI Forms - Bringing logic to UI development

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.

14:00‑15:00 Session 2
Location: AT 2.11
14:00 Henning Christiansen, Christian Theil Have, Ole Torp Lassen and Matthieu Petit
The Viterbi Algorithm expressed in Constraint Handling Rules

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.

14:25 Jon Sneyers (K.U.Leuven)
CHRiSM Introduction

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 in the realm of automated music generation.

14:40 Jon Sneyers
Result-directed CHR Execution

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.

15:30‑17:00 Session 3 (Applications and Demos)
Location: AT 2.11
15:30 Ralf Gerlich
Generic and Extensible Automatic Test Data Generation for Safety Critical Software with CHR

We present a new method for automatic test data generation (ATDG) applying to semantically annotated control flow 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.

A critical problem in ATDG based on coverage goals are so-called infeasible paths, that is, paths in the CFG for which no input exists that leads to their execution. Several different and arbitrarily combinable strategies for construction of paths in the function under test (FUT) have been developed to avoid the construction of such infeasible paths under different circumstances. Results from other analyses --- abstract interpretation, for example --- can be easily integrated.

These strategies include forward and backward prediction control- and data-flow as well as forward and backward execution of the FUT or portions thereof. All of these strategies have been shown to be of advantage in various situations.

The method is new in that it supports the direct use of semantically annotated CFGs, a generic set of coverage criteria and the modular and extensible use of both new and previously-known strategies for path construction and avoidance of infeasible paths at the same time.

CHR allows to carry that modularity and extensibility provided by the theoretical foundation into the actual implementation. Adding strategies is mostly a matter of adding a few new rules. The method also requires both search and probabilistic elements, which were implemented by using the K.U.Leuven optimising CHR compiler in SWI Prolog and combining them with a modified version of PCHR.

A prototype was implemented using CHR both for the path construction as well as the solving of algebraic constraints derived thereof. A toolset for application on a safety-critical software system based on a safe subset of the language C is currently being developed.

Besides ATDG, the method has potential for further applications, for example for worst-case execution time (WCET) analysis required for realtime systems.

We present a short introduction to the method and describe the aspects of its implementation in CHR.

About the company: 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.

15:55 Florian Geiselhart, Frank Raiser, Jon Sneyers and Thom Fruehwirth
MTSeq - multi-touch-enabled music generation and manipulation based on CHR

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 encourages usage of CHR for musicians and other non-computer-scientists. 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.

16:20 Ayman Adel Abdelsamie Abdelaal, Frank Raiser, Thom Frühwirth, and Roland Stelzer
Long-term routing for autonomous sail boats with CHR

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 (http://www.roboat.at/en/home/) and aims to perform long-term routing for fully autonomous sailing boats.

16:45 Peter Van Weert
Conclusions