Abstract
Most symbolic model checkers use BDDs to represent arithmetic constraints over bounded integer variables. The size of such BDDs can be exponential on the number and size (in bits) of the integer variables in the worst case. In this paper we show how to construct linearsized BDDs for linear integer arithmetic constraints. We present basic constructions for atomic equality and inequality constraints and extend them to handle arbitrary linear arithmetic formulas. We also present three alternative ways of handling out-of-bounds transitions, and discuss multiple bounds on integer variables. We experimentally compare our approach to other BDD-based symbolic model checkers and demonstrate that the algorithms presented in this paper can be used to improve their performance significantly.
This work is supported in part by NSF grant CCR-9970976 and NSF CAREER award CCR-9984822.
Chapter PDF
References
Cadence SMV. http://www-cad.eecs.berkeley.edu/~kenmcmil/smv.
G. R. Andrews. Concurrent Programming: Principles and Practice. The Benjamin/ Cummings Publishing Company, Redwood City, California, 1991.
R. Bryant. Graph-based algorithms for boolean function manipulation. In Proceedings of the 27th ACM/IEEE Design Automation Conference, 1990.
R.E Bryant and Y.A. Chen. Verification of arithmetic functions with binary moment diagrams. In Proceedings of the 32nd ACM/IEEE Design Automation Conference, June 1995.
T. Bultan, R. Gerber, and C. League. Composite model checking: Verification with type-specific symbolic representations. ACM Transactions on Software Engineering and Methodology, 9(1):3–50, January 2000.
T. Bultan and T. Yavuz-Kahveci. Action language verifier. In Proceedings of the 16th IEEE International Conference on Automated Software Engineering, 2001.
W. Chan, R. J. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, and J. D. Reese. Model checking large software specifications. IEEE Transactions on Software Engineering, 24(7):498–520, July 1998.
A. Cimatti, E.M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. Nusmv 2: An opensource tool for symbolic model checking. In Proceedings of the International Conference on Computer-Aided Verification, 2002.
E.M. Clarke, M. Fujita, and X. Zhao. Hybrid decision diagrams-overcoming the limitations of mtbdds and bmds. In In International Conference of Computer-Aided Design, pages 159–163, 2000.
M. Garey and D. Jonson. Computers and Intractability: A Guide to the Theory of NP-completeness. Freeman, 1979.
K. L. McMillan. Symbolic model checking. Kluwer Academic Publishers, Massachusetts, 1993.
J. Yang, A. K. Mok, and F. Wang. Symbolic model checking for event-driven real-time systems. ACM Transactions on Programming Languages and Systems, 19(2):386–412, March 1997.
T. Yavuz-Kahveci, M. Tuncer, and T. Bultan. Composite symbolic library. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of Lecture Notes in Computer Science, pages 335–344. Springer-Verlag, April 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bartzis, C., Bultan, T. (2003). Construction of Efficient BDDs for Bounded Arithmetic Constraints. In: Garavel, H., Hatcliff, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2003. Lecture Notes in Computer Science, vol 2619. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36577-X_28
Download citation
DOI: https://doi.org/10.1007/3-540-36577-X_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00898-9
Online ISBN: 978-3-540-36577-8
eBook Packages: Springer Book Archive