NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login
Back to Results
Formal verification of mathematical softwareMethods are investigated for formally specifying and verifying the correctness of mathematical software (software which uses floating point numbers and arithmetic). Previous work in the field was reviewed. A new model of floating point arithmetic called the asymptotic paradigm was developed and formalized. Two different conceptual approaches to program verification, the classical Verification Condition approach and the more recently developed Programming Logic approach, were adapted to use the asymptotic paradigm. These approaches were then used to verify several programs; the programs chosen were simplified versions of actual mathematical software.
Document ID
19850008180
Acquisition Source
Legacy CDMS
Document Type
Contractor Report (CR)
Authors
Sutherland, D. (Odyssey Research Associates, Inc. Ithaca, NY, United States)
Date Acquired
September 5, 2013
Publication Date
May 1, 1984
Subject Category
Computer Programming And Software
Report/Patent Number
NASA-CR-172407
NAS 1.26:172407
Accession Number
85N16489
Funding Number(s)
PROJECT: RTOP 324-01-00-01
CONTRACT_GRANT: NAS1-17579
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.

Related Records

There are no records associated with this record.
No Preview Available