S.M. Sadjadi, S. Chen, et al.
TAPIA 2009
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. © 1976, ACM. All rights reserved.
S.M. Sadjadi, S. Chen, et al.
TAPIA 2009
B.K. Boguraev, Mary S. Neff
HICSS 2000
Michael Ray, Yves C. Martin
Proceedings of SPIE - The International Society for Optical Engineering
Alfonso P. Cardenas, Larry F. Bowman, et al.
ACM Annual Conference 1975