search menu icon-carat-right cmu-wordmark

Formal Verification of Programs

December 1988 Curriculum Module
Alfs T. Berztiss (University of Pittsburgh), Mark A. Ardis (Stevens Institute of Technology)

This 1988 module introduces formal verification of programs, dealing primarily with proofs of sequential programs, but also with consistency proofs for data types and deduction of particular behaviors of programs from their specifications.

Publisher:

Software Engineering Institute

CMU/SEI Report Number

CMU/SEI-88-CM-020

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.