02214oam 2200517 450 991070783470332120161223141253.0(CKB)5470000002468213(OCoLC)844605585(EXLCZ)99547000000246821320130526j199608 ua 0engurbn||||a|a||txtrdacontentcrdamediacrrdacarrierA bitvectors library for PVS /Ricky W. Butler [and four others]Washington, D.C. National Aeronautics and Space Administration1996Hampton, Virginia :National Aeronautics and Space Administration, Langley Research Center,August 1996.1 online resource (17 pages) illustrationsNASA technical memorandum ;110274"August 1996.""Performing organization: National Aeronautics and Space Administration Langley Research Center" Report documentation page.Includes bibliographical references (pages 16-17).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.HardwarenasatProvingnasatBit synchronizationnasatIntegersnasatLibrariesnasatHardware.Proving.Bit synchronization.Integers.Libraries.Butler Ricky W.1398460Langley Research Center,OCLCEOCLCEOCLCOOCLCQGPOBOOK9910707834703321A bitvectors library for PVS3549741UNINA