Abstract
How do you ensure that software does what it's supposed to do? Traditional methods of software verification and validation, based on testing, reviews and analyses, are not always sufficient. Deductive verification goes a step further, establishing true properties of all possible executions of a program, via formal reasoning within an appropriate logic: a program logic.
The first lecture illustrated this approach with the deductive verification of a dichotomous search function in a sorted array, a widely used algorithm that is often incorrectly implemented.
Next, the lecture traced the emergence of deductive verification and program logic via three seminal publications. Alan Turing's brief 1949 paper, " Checking a large routine ", introduced two major ideas: logical assertions and termination orders, and illustrated them on the verification of a small program expressed as a flowchart. Too far ahead of its time, and never formally published, this seminal text fell into oblivion until 1984.
Robert W. Floyd's 1967 article, " Assigning meanings to programs ", reinvents Turing's approach and extends it considerably, with a complete formalization of the verification conditions that guarantee that a program is correctly annotated, and the observation, revolutionary for the time, that such formalization constitutes a formal semantics of the programming language used.
Finally, C. A. R. Hoare's 1969 article " An axiomatic basis for computer programming " is the manifesto of modern deductive verification. The article extends Floyd's results to a language with structured control (sequences, conditionals, loops) and introduces notations still in use today (the "Hoare triplets"). But beyond its technical contributions, this article is visionary both in its purely axiomatic approach to deductive verification and in its lucid analysis of the practical value of this approach.
