Design and Verification of Reliable Software.
Abstract
This research project is concerned with methods for developing provably correct system programs. Two complementary approaches have been pursued. The first is the development of basic tools for describing and verifying concurrent programs; the aim is to find ways of managing the complexity which arises from concurrent interactions between system components. Specification and proof methods for invariant properties of modular programs have been developed. They allow independent verification of each module and provide a sufficient basis for reasoning about a wide class of concurrent systems. Tools for stating and verifying other types of requirements, e.g. that a message is eventually delivered, are in an earlier stage. Techniques have been designed that use temporal logic, a logical system that allows statements about future events.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 01, 1979
- Accession Number
- ADA074224
Entities
People
- Susan S. Owicki
Organizations
- Stanford University