An efficient decision procedure for the theory of fixed-sized bit-vectors

  • David Cyrluk
  • Oliver Möller
  • Harald Rueß
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


In this paper we describe a decision procedure for the core theory of fixed-sized bit-vectors with extraction and composition that can readily be integrated into Shostak's procedure for deciding combinations of theories. Inputs to the solver are unquantified bit-vector equations t=u and the algorithm returns true if t=u is valid in the bit-vector theory, false if t=u is unsatisfiable, and a system of solved equations otherwise. The time complexity of the solver is \(\mathcal{O}\left( {\left| t \right| \cdot log{\text{ }}n + n^2 } \right)\), where t is the length of the bit-vector term t and n denotes the number of bits on either side of the equation. Then, the solver for the core bit-vector theory is extended to handle other bit-vector operations like bitwise logical operations, shifting, and arithmetic interpretations of bit-vectors. We develop a BDD-like data-structure called bit-vector BDDs to represent bit-vectors, various operations on bit-vectors, and a solver on bit-vector BDDs.


Decision Procedure Simple Term Core Theory Core Solver Bitwise Operation 
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. 1.
    R.E. Bryant. Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams. ACM Computing Surveys, 24(3):293–318, September 1992.Google Scholar
  2. 2.
    D. Dill, C. Barrett and J. Levitt. Validity Checking for Combinations of Theories with Equality. In M. Srivas, editor, FMCAD '96, volume 1166 of Lecture Notes in Computer Science, pages 187–201, Palo Alto, CA, November 1996. Springer-Verlag.Google Scholar
  3. 3.
    D. Cyrluk, P. Lincoln, and N. Shankar. On Shostak's Decision Procedure for Combination of Theories. In M. A. McRobbie and J. K. Slaney, editors, Proc. of CADE'96, volume 1104 of Lecture Notes in Artificial Intelligence, pages 463–477, New Brunswick, NJ, July/August 1996. Springer-Verlag.Google Scholar
  4. 4.
    D. Cyrluk, O. Möller, and H. Rueß. An Efficient Decision Procedure for a Theory of Fixed-Sized Bitvectors with Composition and Extraction. Technical report, Universität Ulm, D-89069 Ulm, Oberer Eselsberg, December 1996.Google Scholar
  5. 5.
    S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, February 1995.Google Scholar
  6. 6.
    H. Rueß. Hierarchical Verification of Two-Dimensional High-Speed Multiplication in PVS: A Case Study. In M.K. Srivas and A. Camilleri, editors, Formal Methods in Computer-Aided Design, volume 1166 of Lecture Notes in Computer Science. Springer-Verlag, November 1996.Google Scholar
  7. 7.
    R.E. Shostak. Deciding Combinations of Theories. Journal of the ACM, 31(1):1–12, January 1984.Google Scholar
  8. 8.
    M.K. Srivas and S.P. Miller. Formal Verification of the AAMP5 Microprocessor. In M.G. Hinchey and J.P. Bowen, editors, Applications of Formal Methods, International Series in Computer Science, chapter 7, pages 125–180. Prentice Hall, Hemel Hempstead, UK, 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • David Cyrluk
    • 1
  • Oliver Möller
    • 2
  • Harald Rueß
    • 2
  1. 1.Computer Science LaboratorySRI InternationalMenlo ParkUSA
  2. 2.Fakultät für InformatikUniversität UlmUlmGermany

Personalised recommendations