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

  • William Chan
  • Richard Anderson
  • Paul Beame
  • David Notkin
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


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.


Model Check Boolean Function Boolean Variable Constraint Solver Arithmetic Circuit 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [ABB+96]
    R. J. Anderson, P. Beame, S. Burns, W. Chan, F. Modugno, D. Notkin, and J. D. Reese. Model checking large software specifications. In Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 156–166, October 1996.Google Scholar
  2. [AG93]
    J. M. Atlee and J. Gannon. State-based model checking of event-driven system requirements. IEEE Transactions on Software Engineering, SE-19(1):24–40, January 1993.Google Scholar
  3. [BC95]
    R. E. Bryant and Y.-A. Chen. Verification of arithmetic circuits with Binary Moment Diagrams. In Proceedings of the 32nd ACM/IEEE Design Automation Conference, pages 535–541, June 1995.Google Scholar
  4. [BCG88]
    M. C. Browne, E. M. Clarke, and O. Grümberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59:115–131, 1988.Google Scholar
  5. [BCM+90]
    J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science, pages 428–439. IEEE Computer Society Press, June 1990.Google Scholar
  6. [Bry86]
    R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(6):677–691, August 1986.Google Scholar
  7. [CDV96]
    J. Crow and B. L. Di Vito. Formalizing space shuttle software requirements. In Proceedings of the ACM SIGSOFT Workshop on Formal Methods in Software Practice, pages 40–48, January 1996.Google Scholar
  8. [CFZ95]
    E. M. Clarke, M. Fujita, and X. Zhao. Hybrid Decision Diagrams overcoming the limitations of MTBDDs and BMDs. In 1995 IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, pages 159–163. IEEE Computer Society Press, November 1995.Google Scholar
  9. [EH86]
    E. A. Emerson and J. Y. Halpern. “Sometimes” and “Not Never” revisited: On branching versus linear time temporal logic. Journal of the ACM, 33(1):151–178, 1986.Google Scholar
  10. [Har87]
    D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231–274, 1987.Google Scholar
  11. [HH95]
    T. A. Henzinger and P.-H. Ho. Algorithmic analysis of nonlinear hybrid systems. In Proceedings of the 7th International Conference on Computer Aided Verification, pages 225–238. Springer-Verlag, July 1995.Google Scholar
  12. [LHHR94]
    N. G. Leveson, M. P. E. Heimdahl, H. Hildreth, and J. D. Reese. Requirements specification for process-control systems. IEEE Transactions on Software Engineering, SE-20(9), September 1994.Google Scholar
  13. [LS81]
    R. J. Lipton and R. Sedgewick. Lower bounds for VLSI. In Conference Proceedings of the Thirteenth Annual ACM Symposium on Theory of Computing, pages 300–307, May 1981.Google Scholar
  14. [McM93]
    K. L. McMillan. Symbolic Model Checking. Kluwer, 1993.Google Scholar
  15. [Mil80]
    R. Milner. A Calculus of Communicating Systems. Springer-Verlag, 1980.Google Scholar
  16. [PB94]
    G. Pesant and M. Boyer. QUAD-CLP(IR): Adding the power of quadratic constraints. In Second International Workshop, Principles and Practice of Constraint Programming, pages 95–108. Springer-Verlag, May 1994.Google Scholar
  17. [Tha96]
    J. S. Thathachar. On the limitations of ordered representations of functions. Technical Report CSE-96-09-03, University of Washington, September 1996.Google Scholar
  18. [WME93]
    F. Wang, A. Mok, and E. A. Emerson. Symbolic model checking for distributed real-time systems. In Proceedings of the First International Symposium of Formal Methods Europe, pages 632–651, April 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • William Chan
    • 1
  • Richard Anderson
    • 1
  • Paul Beame
    • 1
  • David Notkin
    • 1
  1. 1.Computer Science and EngineeringUniversity of WashingtonSeattleUSA

Personalised recommendations