# Publication details

##
Towards the verification of concurrent constraint programs in finite domain reasoning

Jörg Würtz

Post-conference workshop at ICLP: Verification and analysis of (concurrent) logic languages, pp. 87--107, June 1994

Combinatorial problems occur quite often in many application areas, e.g. scheduling or cutting stock problems,
and may be specified as problems over finite domains, i.e., the variables
range over a finite subset of the integers.
Our approach taken in the concurrent constraint language Oz is to
support an efficiently
implementable constraint system for constraints 'x in D'.
Using this constraint system, the programmer can add
his own functionality by so called virtual constraints (e.g. 'x =< y').
Because the problem of satisfiability of these more complex constraints is
NP-complete, most of them are implemented incompletely by
using reflecting operators returning the
current minimum and maximum of a variable's domain.
For these programs serving as the core of finite domain reasoning, the
question of verification arises. Verification is complicated
by the operators reflecting the current known information about
variables.
In our approach we translate the computation states into first order
formulas by giving virtual constraints their intended semantics (the
semantics of the corresponding logic constraint).
We prove that for a reduction of computation states Gamma ->
Gamma' the corresponding first order formulas are equivalent with
respect to the intended model. Our approach, which
seems to be very natural in the setting of constraint languages,
succeeds in proving virtual constraints to be correct,
terminating and complete (in the shown example) with respect to an
intended semantics.

Download PDF
Show BibTeX

@INPROCEEDINGS{wuertz:94c,
title = {Towards the verification of concurrent constraint programs in finite domain reasoning},
author = {J{\"o}rg W{\"u}rtz},
year = {1994},
month = {jun},
editor = {"F.S. de Boer and M. Gabbrielli"},
booktitle = {Post-conference workshop at ICLP: Verification and analysis of (concurrent) logic languages},
pages = {"87--107"},
}

Login to edit

Legal notice, Privacy policy