Progress Measures for Verification Involving Nondeterminism

Abstract

Using the notion of progress measures, we give a complete verification method for proving that a program satisfies a property specified by an automaton having bounded nondeterminism. Such automata can express any safety property. Previous methods, which can be derived from the method presented here, either rely on transforming the program or are not complete. (kr)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 30, 1990
Accession Number
ADA228961

Entities

People

  • Fred B. Schneider
  • Nils Klarlund

Organizations

  • Cornell University

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Abstracts
  • Alphabets
  • Automata
  • Automata Theory
  • Classification
  • Computational Complexity
  • Computer Languages
  • Computer Science
  • Computers
  • Information Processing
  • Language
  • Military Research
  • Notation
  • Security
  • Symbols
  • Theoretical Computer Science
  • Universities

Fields of Study

  • Mathematics

Readers

  • Mathematical Modeling and Probability Theory.