Design and Verification of Reliable Software.

Abstract

This research project is concerned with methods for developing provably correct concurrent programs. Two complementary approaches have been pursued. The first is the development of basic tools for describing and verifying concurrent interactions between system components. Specification and proof methods have been developed for both invariant properties and service guarantees of modular programs. They allow independent verification of each module, and provide a basis for reasoning about a wide class of concurrent systems. Statement and verification of service guarantees is made possible by using temporal logic, a logical system in which one can reason about the future states of a program computation.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 29, 1980
Accession Number
ADA082545

Entities

People

  • Susan S. Owicki

Organizations

  • Stanford University

Tags

Communities of Interest

  • Engineered Resilient Systems
  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Air Force
  • Algorithms
  • Communications Protocols
  • Computations
  • Computer Networks
  • Computer Science
  • Computers
  • Consistency
  • Databases
  • Electrical Engineering
  • Electronics Laboratories
  • Information Processing
  • Language
  • Network Protocols
  • Operating Systems
  • Specifications
  • Transmitters

Fields of Study

  • Computer science

Readers

  • Distributed Systems and Data Platform Development
  • Mathematical Modeling and Probability Theory.
  • Software Engineering.