In this paper we present a new system called CDB-PV that uses constraint databases (CDBs) for program verification (PV). The
CDB-PV system was implemented in C++ and tested on several sample programs that are difficult to verify using other methods.
The CDB-PV system also runs efficiently for the sample programs. The CDB-PV approach is similar to abstract interpretation
but it allows non-convex approximations.
This research was supported in part by a NSF grant and a NASA Space and EPSCoR grant.