DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click HERE
to register or log in.
Safety Properties of Terminating and Nonterminating Ada Programs in the State Delta Verification System (SDVS),
AEROSPACE CORP EL SEGUNDO CA ENGINEERING AND TECHNOLOGY GROUP
Pagination or Media Count:
We describe recent enhancements to the implementation of invariance in SDVS, the purpose of the new weaknexttr 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.
APPROVED FOR PUBLIC RELEASE