Abstract
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.
Keywords
CorrectnessComputer scienceProgramming languageLogical analysisProgram analysisTheoretical computer scienceMathematics
Affiliated Institutions
Related Publications
The temporal logic of programs
A unified approach to program verification is suggested, which applies to both sequential and parallel programs. The main proof method suggested is that of temporal reasoning in...
Proof of a program
A proof is given of the correctness of the algorithm “Find.” First, an informal description is given of the purpose of the program and the method used. A systematic technique is...
The structure of “THE”-multiprogramming system
A multiprogramming system is described in which all activities are divided over a number of sequential processes. These sequential processes are placed at various hierarchical l...
The structure of the “THE”-multiprogramming system
A multiprogramming system is described in which all activities are divided over a number of sequential processes. These sequential processes are placed at various hierarchical l...
The teachable language comprehender
The Teachable Language Comprehender (TLC) is a program designed to be capable of being taught to “comprehend” English text. When text which the program has not seen before is in...
Publication Info
- Year
- 1976
- Type
- article
- Volume
- 19
- Issue
- 4
- Pages
- 188-206
- Citations
- 136
- Access
- Closed
External Links
Social Impact
Altmetric
PlumX Metrics
Social media, news, blog, policy document mentions
Citation Metrics
136
OpenAlex
Cite This
Shmuel Katz,
Zohar Manna
(1976).
Logical analysis of programs.
Communications of the ACM
, 19
(4)
, 188-206.
https://doi.org/10.1145/360032.360048
Identifiers
- DOI
- 10.1145/360032.360048