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.
This report is related to the following area(s) of work:
Performance and DependabilityCurriculum Module
CMU/SEI-88-CM-020
December 1988
SEI:
Berztiss, Alfs; & Ardis, Mark. Formal Verification of Programs (CMU/SEI-88-CM-020). Software Engineering Institute, Carnegie Mellon University, 1988. http://www.sei.cmu.edu/library/abstracts/reports/88cm020.cfm
IEEE:
A. Berztiss, and M. Ardis, "Formal Verification of Programs," Software Engineering Institute, Carnegie Mellon University, Pittsburgh, Pennsylvania, Curriculum Module CMU/SEI-88-CM-020, 1988. http://www.sei.cmu.edu/library/abstracts/reports/88cm020.cfm
APA:
Berztiss, A., & Ardis, M. (1988). Formal Verification of Programs (CMU/SEI-88-CM-020). Retrieved May 19, 2013, from the Software Engineering Institute, Carnegie Mellon University website: http://www.sei.cmu.edu/library/abstracts/reports/88cm020.cfm
CHI:
Berztiss, Alfs, and Mark Ardis. Formal Verification of Programs (CMU/SEI-88-CM-020). Pittsburgh, PA: Software Engineering Institute, Carnegie Mellon University, 1988. http://www.sei.cmu.edu/library/abstracts/reports/88cm020.cfm
MLA:
Berztiss, A., & Ardis, M. 1988. Formal Verification of Programs (Technical Report CMU/SEI-88-CM-020). Pittsburgh: Software Engineering Institute, Carnegie Mellon University. http://www.sei.cmu.edu/library/abstracts/reports/88cm020.cfm
For more information