Résumé: The purpose of th]s paper is to point out the sigmficant quantity of work in progress on techmques that will enable programmers to prove their programs correct This work has included: investigations m the theory of program schemas or abstract programs, development of the art of the informal or manual proof of correctness; and development of mechanical or semi-mechanical approaches to proving correctness At present, these mechanical approaches rely upon the availability of powerful theorem-provers, development of which is being actively pursued. All of these technical areas are here surveyed in detail, and recommendatmns are made concerning the direction of future research toward producing a sem~-mechamcal program verifier.

Langue: Anglais