Tools

LEADER 02866nam 2200565 i 4500

001 ocn844605585;

003 OCoLC;

005 20170127102334.0;

006 m o d f ;

007 cr bn||||a|a||;

008 130526e199608 vaua obt f000 0 eng c;

035 a| (Sirsi) o844605585;

042 a| pcc;

049 a| ERE#;

074 a| 0830-D (online);

086 0 a| NAS 1.15:110274;

100 1 a| Butler, Ricky W.,e| author.=| ^A428433;

245 12 a| A bitvectors library for PVS /c| Ricky W. Butler [and four others].;

260 a| Washington, D.C. :b| National Aeronautics and Space Administration,c| 1996.;

264 1 a| Hampton, Virginia :b| National Aeronautics and Space Administration, Langley Research Center,c| August 1996.;

300 a| 1 online resource (17 pages) :b| illustrations.;

336 a| textb| txt2| rdacontent;

337 a| computerb| c2| rdamedia;

338 a| online resourceb| cr2| rdacarrier;

490 1 a| NASA technical memorandum ;v| 110274;

500 a| "August 1996.";

500 a| "Performing organization: National Aeronautics and Space Administration Langley Research Center"--Report documentation page.;

500 a| CRDP Project record.;

504 a| Includes bibliographical references (pages 16-17).;

513 a| Technical memorandum.;

520 a| 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.;

536 a| Sponsored by the National Aeronautics and Space Administrationd| WU 505-64-10-13;

588 a| Description based on online resource; title from PDF title page (NASA, viewed Dec. 23, 2016).;

588 0 a| Print version record.;

650 7 a| Hardware.2| nasat;

650 7 a| Proving.2| nasat;

650 7 a| Bit synchronization.2| nasat;

650 7 a| Integers.2| nasat;

650 7 a| Libraries.2| nasat;

710 2 a| Langley Research Center,e| issuing body.=| ^A192893;

776 08 i| Print version:t| Bitvectors library for PVSw| (OCoLC)70189502;

776 08 i| Microfiche version:t| Bitvectors library for PVSw| (OCoLC)40173207;

830 0 a| NASA technical memorandumv| 110274.=| ^A467613;

856 40 u| https://purl.fdlp.gov/GPO/gpo75879;

949 a| Click on web addressw| asish| joyner94;

998 a| 4617486;

998 a| u4617486;

596 a| 1;

999 a| CLICK ON WEB ADDRESSw| ASISc| 1i| 4617486-1001l| JNETm| JOYNERr| Ys| Yt| JNE1DOu| 1/17/2017x| EDOCUMENTz| JERESOURCE;

A bitvectors library for PVS / Ricky W. Butler [and four others].

Author/creator	Butler, Ricky W. author.
Other author	Langley Research Center, issuing body.
Format	Electronic
Publication Info	Washington, D.C. : National Aeronautics and Space Administration, 1996.
Publication	Hampton, Virginia : National Aeronautics and Space Administration, Langley Research Center, August 1996.
Description	1 online resource (17 pages) : illustrations.
Supplemental Content	https://purl.fdlp.gov/GPO/gpo75879

Series	NASA technical memorandum ; 110274 NASA technical memorandum 110274. ^A467613
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.
General note	"August 1996."
General note	"Performing organization: National Aeronautics and Space Administration Langley Research Center"--Report documentation page.
General note	CRDP Project record.
Bibliography note	Includes bibliographical references (pages 16-17).
Report note	Technical memorandum.
Funding information	Sponsored by the National Aeronautics and Space Administration WU 505-64-10-13
Source of description	Description based on online resource; title from PDF title page (NASA, viewed Dec. 23, 2016).
Source of description	Print version record.
Issued in other form	Print version: Bitvectors library for PVS
Issued in other form	Microfiche version: Bitvectors library for PVS
GPO item number	0830-D (online)
Govt. docs number	NAS 1.15:110274

Availability

Library	Location	Call Number	Status	Item Actions
	Electronic Resources	Access Content Online	✔ Available

A bitvectors library for PVS / Ricky W. Butler [and four others].

Click here for more information about this title

Availability