Safety Properties of Terminating and Nonterminating Ada Programs in the StateDelta Verification System (SDVS)

摘要

We describe recent enhancements to the implementation of invariance in SDVS, thepurpose 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.