Combining constraint solving and symbolic model checking for a class of systems with non-linear constraints

from the Research Page of William Chan

Paper by William Chan, Richard Anderson, Paul Beame, and David Notkin. In Computer Aided Verification, 9th International Conference, CAV'97 Proceedings, LNCS 1254, pages 316-327. Springer-Verlag, June 1997, Haifa, Israel.

Download (12 pages):

Abstract

We extend the conventional BDD-based model checking algorithms 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 correspond to infeasible constraints. We illustrate our technique with a simple example, which has been analyzed with our prototype implementation.

BibTeX entry

@InProceedings( Chan-CAV97,
  title = "Combining Constraint Solving and Symbolic Model Checking for
           a Class of Systems with Non-Linear Constraints", 
  author = "William Chan and Richard Anderson and Paul Beame
            and David Notkin",
  booktitle = "Computer Aided Verification, 9th International Conference,
	       CAV'97 Proceedings",
  pages = "316--327",
  month = jun, 
  year = 1997,
  editor = "Orna Grumberg",
  address = "Haifa, Israel",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = 1254
)

William Chan (wchan@cs.washington.edu)