"Program Verification - Theory and Application"
Joe Sremack 2002
Abstract
Knowledge of a program's behavior is extremely helpful for trusting programs, such as those used by NASA. Often utilized in acquiring this knowledge is program verification: the process of using logical and mathematical methods to verify a program's behavior. This paper aims to investigate program verification from both a practical and a philosophical standpoint. The practical goal is to present and demonstrate two of the major verification techniques and the use of theorem provers as verification tools is discussed. Philosophically, the goal is to refute attacks on program verification, and to put forth a positive theory of program verification. Another aim is to dissolve several other philosophical issues threatening program verification, such as Godel's incompleteness theorem and the use of undecidability. Together, the practical and the philosophical discussions provide a thorough account of program verification.