Non-monotonic concurrent constraint program verification using phase semantics.

Abstract

We present two kinds of Concurrent Constraint Programming languages. The first one is based on a classical logic framework, whereas the second one is based on linear logic. The latter will be at the center of our present discussion since it provides several features such as ability to consume constraints and a full translation of the language into the underlying logic. The provability semantics of this logic can then be used to test programs for safety properties. We will also investigate ways of automating this verification technique, notably by means of finite models of the logic.