Deductive Software Verification

  • Doron A. Peled
Part of the Texts in Computer Science book series (TCS)


In the late 1960’s, several researchers, in particular Floyd [45] and Hoare [63], 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 [85] 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.


Model Check Proof System Outgoing Edge Array Variable Total Correctness 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Further Reading

Two concise papers that survey the Hoare verification approach were written by K.R. Apt:

  1. K.R. Apt, Ten years of Hoare’s logic: A survey, part I, Transactions on Programming Languages and Systems, 3 (4), 1981, 431–383.zbMATHCrossRefGoogle Scholar
  2. K.R. Apt, Ten years of Hoare’s logic: A survey, part II: Nondeterminism, Theoretical Computer Science 28, 1984, 83–109.zbMATHMathSciNetCrossRefGoogle Scholar

There are several books on Hoare style deductive theorem proving, including

  1. N. Francez, Program Verification, Addison Wesley, 1992.Google Scholar
  2. K. R. Apt, E.-R. Olderog, Verification of Sequential and Concurrent Programs, Springer-Verlag, 1991 (second edition, 1997 ).Google Scholar
  3. F.B. Schneider, On Concurrent Programming, Springer-Verlag, 1997.Google Scholar

The latter covers also the Manna-Pnueli style verification method. A comprehensive book on the temporal verification of safety properties is

  1. 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.

  1. F. Kröger, Temporal Logic of Programs, EATCS Monographs on Theoretical Computer Science, Springer-Verlag, 1992.Google Scholar

Copyright information

© Lucent Technologies 2001

Authors and Affiliations

  • Doron A. Peled
    • 1
  1. 1.Computing SciencesBell Labs/Lucent TechnologiesMurray HillUSA

Personalised recommendations