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.
Supported by a Microsoft Graduate Fellowship
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
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.
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.
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.
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.
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.
R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(6):677–691, August 1986.
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.
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.
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.
D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231–274, 1987.
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.
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.
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.
K. L. McMillan. Symbolic Model Checking. Kluwer, 1993.
R. Milner. A Calculus of Communicating Systems. Springer-Verlag, 1980.
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.
J. S. Thathachar. On the limitations of ordered representations of functions. Technical Report CSE-96-09-03, University of Washington, September 1996.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chan, W., Anderson, R., Beame, P., Notkin, D. (1997). Combining constraint solving and symbolic model checking for a class of systems with non-linear constraints. In: Grumberg, O. (eds) Computer Aided Verification. CAV 1997. Lecture Notes in Computer Science, vol 1254. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63166-6_32
Download citation
DOI: https://doi.org/10.1007/3-540-63166-6_32
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63166-8
Online ISBN: 978-3-540-69195-2
eBook Packages: Springer Book Archive