USA flag logo/image

An Official Website of the United States Government

FORMAL VERIFICATION FOR C WITH UNIX

Award Information

Agency:
National Aeronautics and Space Administration
Branch:
N/A
Award ID:
12046
Program Year/Program:
1990 / SBIR
Agency Tracking Number:
12046
Solicitation Year:
N/A
Solicitation Topic Code:
N/A
Solicitation Number:
N/A
Small Business Information
ATC - NY
33 Thornwood Drive, Suite 500 Ithaca, NY 14850-
View profile »
Woman-Owned: No
Minority-Owned: No
HUBZone-Owned: No
 
Phase 1
Fiscal Year: 1990
Title: FORMAL VERIFICATION FOR C WITH UNIX
Agency: NASA
Contract: N/A
Award Amount: $49,984.00
 

Abstract:

WE PROPOSE TO BUILD AN AUTOMATED FORMAL VERIFICATION SYSTEM FOR PROGRAMS WRITTEN IN THE C PROGRAMMING LANGUAGE. THIS SYSTEM WILL SUPPORT VERIFICATION OF PROGRAMS THAT INCLUDE UNIX SYSTEM CALLS, INCLUDING THOSE WHICH MAKE POSSIBLE CONCURRENT EXECUTION, SUCH AS FORK AND PIPE. IT WILL ALSO SUPPORT VERIFICATION OF PROGRAMS THAT DO FLOATING POINT ARITHMETIC. THE VERIFIER WILL BE BASED ON AN OPERATIONAL SEMANTICS, WHICH IS POWERFUL, EASY TO UNDERSTAND, AND EASY TO USE. VERIFYING A PROGRAM WITH THIS SYSTEM WILL BE SIMILAR TO SYMBOLIC EXECUTION. WE EXPECT THE SYSTEM TO BE EASY ENOUGH TO USE THAT IT CAN BE USED AS A ROUTINE DEBUGGING TOOL. THE SYSTEM WILL BE BASED ON THE ARIEL PROTOTYPE C VERIFICATION SYSTEM DEVELOPED AT ODYSSEY. THE WORK THAT MUST BE DONE BY THIS PROJECT IS TO SUPPORT FULL C, INCLUDINGI/O AND DEVELOP AND IMPLEMENT SEMANTICS FOR UNIX SYSTEM CALLS, INCLUDING THE TYPE OF CONCURRENT PROGRAMMING THAT IS POSSIBLE IN UNIX.

Principal Investigator:

Douglas N. Hoover
Logician
6072772020

Business Contact:

Kenneth r. morin
DIRECTOR OF FINANCE
6072772020
Small Business Information at Submission:

Odyssey Research Assocs Inc
301-a Harris B. Dates Drive Ithaca, NY 14850

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