Software Engineering Institute | Carnegie Mellon University
Software Engineering Institute | Carnegie Mellon University

Digital Library

Javascript is currently disabled for your browser. For an optimal search experience, please enable javascript.

Advanced Search

Basic Search

Content Type

Topics

Publication Date

Curriculum Module

Formal Specification and Verification of Concurrent Programs

  • February 1993
  • By Dan Berry
  • This 1993 module introduces formal specification of concurrent software and verification of the consistency between concurrent programs and their specifications.
  • Performance and Dependability
  • Publisher: Software Engineering Institute
    CMU/SEI Report Number: CMU/SEI-93-CM-027
  • Abstract

    This module introduces formal specification of concurrent software and verification of the consistency between concurrent programs and their specifications. First, what one might want to be able to prove about a concurrent program is discussed. Then, a number of formal descriptions of the concept are presented. These vary in their coverage of the phenomena, and some can be used as the bases of formal specification of programs. Next, techniques for carrying out the proof of consistency between the specification and the program are described. Finally, it is noted that some of the these techniques have automated tools such as verifiers associated with them.

  • Download