*Universität Ulm, Fakultät für Informatik, Abt.
KI* - Our Papers on Using PVS

## An Efficient Decision Procedure for a Theory of Fixed-Sized
Bitvectors with Composition and Extraction

**D. Cyrluk, O. Möller, H. Rueß**

**Technical Report UIB-96-8, Universität Ulm, Fakultät für Informatik, Dec. 1996**

**Abstract**

The theory of fixed-sized bitvectors with composition and extraction
has been shown to be useful in the realm of hardware verification, and
in this paper we develop an efficient algorithm for deciding this theory.
A proper input is an unquantified bitvector equation, say *t = u*,
and our algorithm returns **true** if *t = u* is valid in the bitvector
theory, **false** if *t = u* is unsatisfiable, and a system of
solved equations otherwise. The time complexity of this solver is *O(|t|
log(n) + n^2)*, where *|t|* is the length of the bitvector term
*t* and *n* denotes the number of bits on either side of the
equation. Moreover, the resulting procedure can readily be integrated into
Shostak's procedure for deciding combinations of theories.

Available as Postscript
(280 KB) or compressed
Postscript (107 KB).

**BibTeX Entry**

@TechReport{CMR96,
author = "D. Cyrluk and O. M{\"o}ller and H. Rue{\ss}",
title = "An {E}fficient {D}ecision {P}rocedure
for a {T}heory of {F}ixed-{S}ized {B}itvectors
with Composition and Extraction",
year = "1996",
number = "96-8",
institute = "Universit{\"a}T Ulm, Fakult{\"a}t f{\"u}r Informatik",
type = "Ulmer Informatik-Berichte"
}

Harald Rueß - March 4, 1997 - Mail
to Webmaster