FORMAL VERIFICATION FOR C WITH UNIX

Award Information
Agency:
National Aeronautics and Space Administration
Branch
n/a
Amount:
$49,984.00
Award Year:
1990
Program:
SBIR
Phase:
Phase I
Contract:
n/a
Award Id:
12046
Agency Tracking Number:
12046
Solicitation Year:
n/a
Solicitation Topic Code:
n/a
Solicitation Number:
n/a
Small Business Information
Odyssey Research Assocs Inc (Currently ATC-NY, INC.)
301-a Harris B. Dates Drive, Ithaca, NY, 14850
Hubzone Owned:
N
Minority Owned:
N
Woman Owned:
N
Duns:
n/a
Principal Investigator:
Douglas N. Hoover
Logician
(607) 277-2020
Business Contact:
KENNETH R. MORIN
DIRECTOR OF FINANCE
(607) 277-2020
Research Institution:
n/a
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.

* information listed above is at the time of submission.

Agency Micro-sites


SBA logo

Department of Agriculture logo

Department of Commerce logo

Department of Defense logo

Department of Education logo

Department of Energy logo

Department of Health and Human Services logo

Department of Homeland Security logo

Department of Transportation logo

Enviromental Protection Agency logo

National Aeronautics and Space Administration logo

National Science Foundation logo
US Flag An Official Website of the United States Government