Abstract
We develop a new, efficient, and compact decision procedure for fixed size bit-vectors with bit-wise boolean operations. The algorithm is designed such that it can also decide some common cases of parameterized (non-fixed) size. To handle even more parameterized cases for bit-vectors without bit-wise boolean operations we devise a unification based algorithm which invokes the first algorithm symbolically on parameters of the form aN + b, where a and b are integers and N is the only unknown.
Our procedures are designed to be integrated in the Shostak combination of decision procedures. This allows them to be tightly integrated with decision procedures for other theories in STeP's (the Stanford Temporal Prover) simplifier and validity checker.
This research was supported in part by the National Science Foundation under grant CCR-95-27927, the Defense Advanced Research Projects Agency under NASA grant NAG2-892, ARO under grant DAAH04-95-1-0317, ARO under MURI grant DAAH04-96-1-0341, and by Army contract DABT63-96-C-0096 (DARPA).
Chapter PDF
Keywords
- Unification Algorithm
- Proof Obligation
- Verification Condition
- Chinese Remainder Theorem
- Linear Arithmetic
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
Baader, F., and Siekmann, J. Unification theory. In Handbook of Logic in Artificial Intelligence and Logic Programming, D. Gabbay, C. Hogger, and J. Robinson, Eds. Oxford University Press, Oxford, UK, 1993.
Basin, D., and Klarlund, N. Hardware verification using monadic second-order logic. In CAV'95 (1995), vol. 939 of LNCS, pp. 31–41.
BjØrner, N. S., Browne, A., Chang, E. S., Colon, M., Kapur, A., Manna, Z., Sipma, H. B., and Uribe, T. E. STeP: Deductive-algorithmic verification of reactive and real-time systems. In CAV'96 (1996), vol. 1102 of LNCS, pp. 415–418.
BjØrner, N. S., Stickel, M. E., and Uribe, T. E. A practical integration of first-order reasoning and decision procedures. In CADE'97 (1997), vol. 1249 of LNCS, pp. 101–115.
Bratsch, A., Eveking, H., Färber, H.-J., and Schellin, U. Lovert — A Logic Verifier of Register-Transfer Level Descriptions. In IMEC-IFIP (1989), L. Claesen, Ed., Elsevier.
Bryant, R. E. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers C-S5, 8 (1986), 677–691.
Bryant, R. E., and Chen, Y.-A. Verification of arithmetic circuits with binary moment diagrams. In DAC'95 (1995).
Comon, H., Dauchet, M., Gilleron, R., Lugiez, D., Tison, S., and Tommasi, M. Tree Automata Techniques and Applications. Obtainable from http://13ux02.univ-lille3.fr/tata/, 1998.
Cooper, D. C. Theorem proving in arithmetic without multiplication. In Machine Intelligence, vol. 7. American Elsevier, 1972, pp. 91–99.
Cyrluk, D., Lincoln, P., and Shankar, N. On Shostak's decision procedure for combinations of theories. In CADE'96 (1996), vol. 1104 of LNCS, pp. 463–477.
Cyrluk, D., Möller, O., and Ruess, H. An efficient decision procedure for the theory of fixed-sized bit-vectors. In CAV'97 (1997), vol. 1254 of LNCS, pp. 60–71.
Jaffar, J. Minimal and complete word unification. J. ACM 37, 1 (1990), 47–85.
Kamerer, J. Bus scheduler verification using STeP. Unpublished report, 1996.
Martelli, A., and Montanari, U. An efficient unification algorithm. ACM Trans. Prog. Lang. Sys. 4, 2 (1982), 258–282.
Nelson, G., and Oppen, D. C. Simplification by cooperating decision procedures. ACM Trans. Prog. Lang. Sys. 1, 2 (1979), 245–257.
Niven, I., Zuckerman, H., and Montgomery, H. An Introduction to the Theory of Numbers. John Wiley & Sons, New York, 1991.
Shostak, R. E. Deciding combinations of theories. J. ACM 31, 1 (1984), 1–12.
Sipma, H. B., Uribe, T. E., and Manna, Z. Deductive model checking. In CAV'96 (1996), vol. 1102 of LNCS, pp. 208–219.
Stockmeyer, L. J., and Meyer, A. R. Word problems requiring exponential time. In Proc. 5rd ACM Symp. Theory of Comp. (1973), pp. 1‥
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
BjØrner, N.S., Pichora, M.C. (1998). Deciding fixed and non-fixed size bit-vectors. In: Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1998. Lecture Notes in Computer Science, vol 1384. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054184
Download citation
DOI: https://doi.org/10.1007/BFb0054184
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64356-2
Online ISBN: 978-3-540-69753-4
eBook Packages: Springer Book Archive