Sai Zeng, Angran Xiao, et al.
CAD Computer Aided Design
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.
Sai Zeng, Angran Xiao, et al.
CAD Computer Aided Design
Khaled A.S. Abdel-Ghaffar
IEEE Trans. Inf. Theory
Frank R. Libsch, Takatoshi Tsujimura
Active Matrix Liquid Crystal Displays Technology and Applications 1997
Michael C. McCord, Violetta Cavalli-Sforza
ACL 2007