1997 | ReviewPaper | Buchkapitel
An efficient decision procedure for the theory of fixed-sized bit-vectors
verfasst von : David Cyrluk, Oliver Möller, Harald Rueß
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.