Deciding fixed and non-fixed size bit-vectors
NS Bjørner, MC Pichora - … Conference on Tools and Algorithms for the …, 1998 - Springer
NS Bjørner, MC Pichora
International Conference on Tools and Algorithms for the Construction and …, 1998•SpringerWe 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 …
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 …
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.
Springer
Showing the best result for this search. See all results