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