the current state of proving programs correct
Presented are successful efforts in proving that computer programs are correct. Included are (i) the methods used, (ii) the wide class of programs (including systems programs) that have been proved, and (iii) implemented computer systems for demonstrating correctness. There is also a partially annotated bibliography.
program correctness computation method class systems survey reliability inductive assertions verification verifier tutorial program proving proof methods assertions proof algorithm proof proof checker software reliability