Verifying Safety Properties Using Non-Deterministic Infinite-State Automata

Abstract

A new class of infinite-state automata, called safety automata, is introduced. Any safety property can be specified by using such an automation. Sound and complete proof obligations for establishing that an implementation satisfies the property specified by a safety automaton are given. Keywords: Computer program verification, Concurrent programming, Temporal logic.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 08, 1989
Accession Number
ADA212598

Entities

People

  • Fred B. Schneider
  • Nils Klarlund

Organizations

  • Cornell University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Automata
  • Availability
  • Classification
  • Computer Science
  • Decomposition
  • Language
  • Military Research
  • Neurobehavioral Manifestations
  • Notation
  • Plastic Explosives
  • Security
  • Sequences
  • Specifications
  • Transitions
  • Universities
  • Verification

Fields of Study

  • Computer science
  • Engineering

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Aviation Safety Risk Assessment.
  • Neural Network Machine Learning.