Logical Analysis of Programs Most present systems for verification of computer programs are incomplete in that intermediate inductive assertions must be provided manually by the user, termination is not proven, and incorrect programs are not treated. As a unified solution to these problems, this paper suggests conducting a logical analysis of programs by using invariants which express what is actually occurring in the program. The first part of the paper is devoted to techniques for the automatic generation of invariants. The second part provides criteria for using the invariants to check simultaneously for correctness (including termination) or incorrectness. A third part examines the implications of the approach for the automatic diagnosis and correction of logical errors. CACM April, 1976 Katz, S. Manna, Z. logical analysis, invariants, program verification, correctness, incorrectness, termination, automatic debugging 3.66 4.42 5.24 CA760405 JB January 4, 1978 4:15 PM 2871 5 2871 2871 5 2871 2871 5 2871 2874 5 2871 1682 6 2871 2227 6 2871 2317 6 2871 2683 6 2871 2871 6 2871 521 6 2871