USA flag logo/image

An Official Website of the United States Government

THE PRINCIPAL TECHNICAL OBJECTIVE IN THIS PROJECT IS TO SHOWTHE FEASIBILITY OF…

Award Information

Agency:
National Aeronautics and Space Administration
Branch:
N/A
Award ID:
615
Program Year/Program:
1983 / SBIR
Agency Tracking Number:
615
Solicitation Year:
N/A
Solicitation Topic Code:
N/A
Solicitation Number:
N/A
Small Business Information
ATC-NY
33 Thornwood Dr., Suite 500 Ithaca, NY -
View profile »
Woman-Owned: No
Minority-Owned: No
HUBZone-Owned: No
 
Phase 1
Fiscal Year: 1983
Title: THE PRINCIPAL TECHNICAL OBJECTIVE IN THIS PROJECT IS TO SHOWTHE FEASIBILITY OF BUILDING TOOLS TO SUPPORT THE FORMAL VERIFICATION OF MATHEMATICAL SOFTWARE.
Agency: NASA
Contract: N/A
Award Amount: $50,000.00
 

Abstract:

THE PRINCIPAL TECHNICAL OBJECTIVE IN THIS PROJECT IS TO SHOWTHE FEASIBILITY OF BUILDING TOOLS TO SUPPORT THE FORMAL VERIFICATION OF MATHEMATICAL SOFTWARE. NO EXISTING VERIFICATION ENVIRONMENT SUPPORTS PROOF OF CORRECTNESS OF PROGRAMS EXECUTING OVER THE DATA STRUCTURE OF THE REAL NUMBER SYSTEM. THERE ARE ALSO VERY FEW INFORMAL COREECTNESS PROOFS OR EVEN THEORETICAL WORK IN THIS AREA. THIS APPROACH IS MULT-TASKED. IT EXAMINES PROOFS OVER THE ABSTRACT MATHEMATICAL REAL NUMBERS AND CLASSIFIES SOFTWARE AS TO THE AMOUNT OF KNOWLEDGE OF THE THEORY OF THE REAL NUMBERS NECESSARY FOR CORRECTNESS PROOFS. THIS STUDY IS PARTICULARLY INTERESTED IN FRAGMENTS OF ANLYSIS WHICH HAVE FAST LOGICAL DECISION PROCEDURES. IT THEN DEVELOPS MODELS AXIOMS FOR THE MACHINE REPRESENTABLE REAL NUMBERS. THE AXIOMS ARE REFLECTIVE OF THE PHENOMENA OF ROUNDOFF, UNDERFLOW AND OVERFLOW. THEN BEGINS THE STUDY OF PROOFS OF CORRECTNESS OF PROGRAMS WITH RESPECT TO THESE NEW AND MORE REALISTIC AXIOMS. IN ADDITION WE BEGIN THE DEVELOPMENT OF A METHODOLOGY BASED ON INCREMENTAL CONCSTRUCTION OF PROGRAMS AND ATTACHED ASSERTIONS. SUCH AN APPROACH, IF SUCCESSFUL, ERASES THE BURDEN ON A NON-EXPERT USER.

Principal Investigator:

Richard platek
PRINCIPAL INVESTIGATOR

Business Contact:

Small Business Information at Submission:

Odyssey Research Associates
609 W. Clinton St. Ithaca, NY 14850

EIN/Tax ID:
DUNS: N/A
Number of Employees: N/A
Woman-Owned: No
Minority-Owned: No
HUBZone-Owned: No