Combining Constraint Solving and Symbolic Model Checking for a Class of Systems with Non-Linear Constraints

Abstract. We extend the conventional BDD-based model checking al-gorithms to verify systems with non-linear arithmetic constraints. We represent each constraint as a BDD variable, using the information from a constraint solver to prune the BDDs by removing paths that corre-spond to infeasible constraints. We illustrate our technique with a simple example, which has been analyzed with our prototype implementation.