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