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

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 30, 1992
Accession Number
ADA288812

Entities

People

  • T. K. Menas

Organizations

  • The Aerospace Corporation

Tags

Communities of Interest

  • Space

DTIC Thesaurus Topics

  • Abstracts
  • Computer Science
  • Computers
  • Coverings
  • Engineering
  • Intervals
  • Invariance
  • Language
  • National Security
  • Security
  • Standards
  • Time Intervals
  • Translators
  • Verification

Fields of Study

  • Physics

Readers

  • Computer Science.
  • Educational Psychology
  • Mathematical Modeling and Probability Theory.