Advanced Search

Content Type

Topics

Publication Date

Formal Specification and Verification of Concurrent Programs

  • Author(s):
  • Publish Date:
  • Publisher: Software Engineering Institute
  • SEI Identifier: CMU/SEI-93-CM-027
  • Type: Curriculum Module
  • Topics: Performance and Dependability
  • Description: This 1993 module introduces formal specification of concurrent software and verification of the consistency between concurrent programs and their specifications.

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.

Cite This Report

Show Citation Formats

SEI

Berry, Daniel. Formal Specification and Verification of Concurrent Programs (CMU/SEI-93-CM-027). Software Engineering Institute, Carnegie Mellon University, 1993. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=11767

IEEE

Berry. Daniel, "Formal Specification and Verification of Concurrent Programs," Software Engineering Institute, Carnegie Mellon University, Pittsburgh, Pennsylvania, Curriculum Module CMU/SEI-93-CM-027, 1993. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=11767

APA

Berry, Daniel. (1993). Formal Specification and Verification of Concurrent Programs (CMU/SEI-93-CM-027). Retrieved July 23, 2014, from the Software Engineering Institute, Carnegie Mellon University website: http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=11767

CHI

Daniel Berry. Formal Specification and Verification of Concurrent Programs (CMU/SEI-93-CM-027). Pittsburgh, PA: Software Engineering Institute, Carnegie Mellon University, 1993. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=11767

MLA

Berry, Daniel. 1993. Formal Specification and Verification of Concurrent Programs (Technical Report CMU/SEI-93-CM-027). Pittsburgh: Software Engineering Institute, Carnegie Mellon University. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=11767