Advanced Search

Content Type

Topics

Publication Date

Formal Verification of Programs

Abstract

This module introduces formal verification of programs. It deals primarily with proofs of sequential programs, but also with consistency proofs for data types and deduction of particular behaviors of programs from their specifications. Two approaches are considered: verification after implementation that a program is consistent with its specification, and parallel development of a program and its specification. An assessment of formal verification is provided.

Cite This Report

Show Citation Formats

SEI

Berztiss, Alfs; & Ardis, Mark. Formal Verification of Programs (CMU/SEI-88-CM-020). Software Engineering Institute, Carnegie Mellon University, 1988. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=10545

IEEE

Berztiss. Alfs, and Ardis. Mark, "Formal Verification of Programs," Software Engineering Institute, Carnegie Mellon University, Pittsburgh, Pennsylvania, Curriculum Module CMU/SEI-88-CM-020, 1988. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=10545

APA

Berztiss, Alfs., & Ardis, Mark. (1988). Formal Verification of Programs (CMU/SEI-88-CM-020). Retrieved November 01, 2014, from the Software Engineering Institute, Carnegie Mellon University website: http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=10545

CHI

Alfs Berztiss, & Mark Ardis. Formal Verification of Programs (CMU/SEI-88-CM-020). Pittsburgh, PA: Software Engineering Institute, Carnegie Mellon University, 1988. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=10545

MLA

Berztiss, Alfs., & Ardis, Mark. 1988. Formal Verification of Programs (Technical Report CMU/SEI-88-CM-020). Pittsburgh: Software Engineering Institute, Carnegie Mellon University. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=10545