Using Constraints to Verify Properties of Rule Programs

Rule-based programming has been gaining interest in the industry for several years, through the growing use of Business Rules Management Systems. A demand for verification of semantic properties on rule programs has thus emerged. In this paper we present an approach to rule program verification, using constraints to model program executions and verification properties, and a Constraint-Based Programming Solver (CP Solver) to compute the answers to verification questions. We also study the use of constraint-based programming in rule program verification, and the consequences of this usage on the CP Solver compared to combinatorial optimization problems.