Tools and Rules for the Practicing Verifier

Abstract

The paper presents a minimal proof theory which is adequate for proving the main important temporal properties of reactive programs. The properties we consider consist of the classes of invariance, response, and precedence properties. For each of these classes we present a small set of rules that is complete for verifying properties belonging to this class. We illustrate the application of these rules by analyzing and verifying the properties of a new algorithm for mutual exclusion.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jul 03, 1990
Accession Number
ADA227320

Entities

People

  • Amir Pnueli
  • Zohar Manna

Organizations

  • Stanford University

Tags

DTIC Thesaurus Topics

  • Air Force
  • Algorithms
  • Applied Mathematics
  • California
  • Computations
  • Computer Science
  • Construction
  • European Communities
  • Intervals
  • Invariance
  • Language
  • Notation
  • Sequences
  • Transitions
  • United States
  • Urban Areas
  • Verification

Fields of Study

  • Computer science

Readers

  • Mathematical Modeling and Probability Theory.