Accession Number : ADA288812

Title :   Safety Properties of Terminating and Nonterminating Ada Programs in the State Delta Verification System (SDVS),

Corporate Author : AEROSPACE CORP EL SEGUNDO CA ENGINEERING AND TECHNOLOGY GROUP

Personal Author(s) : Menas, T. K.

PDF Url : ADA288812

Report Date : 30 SEP 1992

Pagination or Media Count : 41

Abstract : We describe recent enhancements to the implementation of invariance in SDVS, the purpose of the new weaknext^tr flag, and enhancements to the omegainduct command. We use these enhancements to SDVS to prove a safety property of both a terminating and a nonterminating Ada program.

Descriptors :   *COMPUTER PROGRAM VERIFICATION, *ADA PROGRAMMING LANGUAGE, *SYSTEM SAFETY, MODIFICATION, INVARIANCE.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE