NASA NTRS · 19970001377
A Bitvectors Library for PVS
Abstract
This paper describes a bitvectors library that has been developed for PVS. The library defines a bitvector as a function from a subrange of the integers into (0,1). The library provides functions that interpret a bitvector as a natural number, as a 2's complement number, as a vector of logical values and as a 2's complement fraction. The library provides a concatenation operator and an extractor. Shift, extend and rotate operations are also, defined. Fundamental properties of each of these operations have been proved in PVS.
Keep this discovery
Explore connections, maps & timelines
Butler, Ricky W., Miner, Paul S., Srivas, Mandayam K., Greve, Dave A., Miller, Steven P.. 1996-08-01. A Bitvectors Library for PVS. https://ntrs.nasa.gov/citations/19970001377
Cite the original work for its findings. Save a collection to share your selection of sources.