Formal Specification of IEEE Floating-Point Arithmetic Using PVS

Autor:	Paul S. Miner
Rok vydání:	1995
Předmět:	Floating point Basis (linear algebra) Programming language Generalization Computer science Binary number computer.software_genre Formal methods IEEE floating point Formal specification Prototype Verification System Hardware_ARITHMETICANDLOGICSTRUCTURES Arithmetic computer
Zdroj:	IFAC Proceedings Volumes. 28:31-36
ISSN:	1474-6670
DOI:	10.1016/s1474-6670(17)44820-8
Popis:	A significant portion of the ANSI/IEEE-854 Standard for Radix-Independent Floating Point Arithmetic is fonnally defined using PVS (Prototype Verification System). Since IEEE-854 is a generalization of the ANSI/IEEE-754 Standard for Binary Floating-Point Arithmetic, the PVS specification also formally defines much of IEEE-754. This collection of PVS theories provides a basis for machine checked verification of floating-point systems. The process of defining IEEE-854 using PVS revealed some imprecision in the standard. This formal definition illustrates that formal specification techniques are sufficiently advanced that it is reasonable to consider their use in the development of future standards.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::da5026bff92e452a254026b56efa19ba https://doi.org/10.1016/s1474-6670(17)44820-8 Zobrazit plný text záznamu