Deductive Software Verification
In the late 1960’s, several researchers, in particular Floyd  and Hoare , advocated the idea of formally verifying algorithms and computer programs. The techniques developed involved formalisms that combine program text and logic, used within specially developed proof systems. Later works considered the addition of various programming constructs such as array variables and procedure calls  and concurrency [86, 108]. It was also suggested that such proof systems will be used in the opposite way: applying methods and tools related to deductive verification to develop provably correct programs from a given specification. A collection of powerful mechanized theorem provers have been developed recently (see a list of some of these tools at the end of this chapter). These can assist in obtaining correctness proofs and enforcing the correct use of deductive verification.
KeywordsModel Check Proof System Outgoing Edge Array Variable Total Correctness
Unable to display preview. Download preview PDF.
Two concise papers that survey the Hoare verification approach were written by K.R. Apt:
There are several books on Hoare style deductive theorem proving, including
The latter covers also the Manna-Pnueli style verification method. A comprehensive book on the temporal verification of safety properties is
- Z. Manna, A. Pnueli, Temporal Verification of Reactive Systems: Safety, Springer-Verlag, 1995.Google Scholar
The book by Kräger also describes the temporal verification approach.
- F. Kröger, Temporal Logic of Programs, EATCS Monographs on Theoretical Computer Science, Springer-Verlag, 1992.Google Scholar