NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
A High-Level Formalization of Floating-Point Number in PVSWe develop a formalization of floating-point numbers in PVS based on a well-known formalization in Coq. We first describe the definitions of all the needed notions, e.g., floating-point number, format, rounding modes, etc.; then, we present an application to polynomial evaluation for elementary function evaluation. The application already existed in Coq, but our formalization shows a clear improvement in the quality of the result due to the automation provided by PVS. We finally integrate our formalization into a PVS hardware-level formalization of the IEEE-854 standard previously developed at NASA.
Document ID
20070003560
Acquisition Source
Langley Research Center
Document Type
Contractor Report (CR)
Authors
Boldo, Sylvie
(Ecole Normale Superieure Lyon, France)
Munoz, Cesar
(National Inst. of Aerospace Hampton, VA, United States)
Date Acquired
August 24, 2013
Publication Date
October 1, 2006
Subject Category
Computer Programming And Software
Report/Patent Number
NIA-Rept-2006-01
NASA/CR-2006-214298
Funding Number(s)
CONTRACT_GRANT: NCC1-02043
PROJECT: NIA-Proj. 2204
WBS: WBS 23-065-10-22
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.
No Preview Available