Résumé: The origins of software verification go back to the pioneers of Computing Science, von Neumann and Turing. The idea has been rediscovered several times since then, for example by McCarthy, Naur and Floyd. The ideals of verification have inspired half a century of productive computing research at the foundations of the subject. There are now flourishing research schools in computational logic, computer-aided proof, programming theory, formal semantics, specification and programming languages, programming methodology and software engineering. By the end of the last century, enormous progress had been made in verification theory and in tools to assist in its application. The technology of proof was extended to include constraint solving and model checking, which were routinely exploited in the electronics industry to increase confidence in the absence of errors in circuit designs before commitment to silicon. Programming theory and semantics provided logics for proof of correctness of well-structured sequential programs. The foundations of concurrent programming were explored by employing temporal logic, and communication over channels was explored in a number of process algebras. Formal specifications were used in certain safety-critical applications as an aid to system development and verification of correctness. Internal program specifications in the form of program assertions were used in the software industry as test oracles, to detect and diagnose errors in regression tests conducted overnight. In suitable cases they are left in customer code for re-checking at run time. The early years of the current century have seen a dramatic spurt in progress towards realization of the ideal of verification of software as well as hardware. Proof technology is now routinely exploited in industrially supported program analysis tools, which successfully detect many kinds of generic program error even before a program is tested. Mature proof tools, both automatic and interactive, are now providing indispensable aid in computing research, including research into verification. For mechanized proof of classical conjectures in mathematics, computers have become an indispensable tool.

Langue: Anglais