A High-Level Formalization of Floating-Point Number in PVS
United States: NASA Center for Aerospace Information (CASI), 2006
Online
report
We 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.
Titel: |
A High-Level Formalization of Floating-Point Number in PVS
|
---|---|
Autor/in / Beteiligte Person: | Boldo, Sylvie ; Munoz, Cesar |
Link: | |
Veröffentlichung: | United States: NASA Center for Aerospace Information (CASI), 2006 |
Medientyp: | report |
Schlagwort: |
|
Sonstiges: |
|