Access Restriction

Author Manna, Zohar ♦ Katz, Shmuel
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Language English
Subject Keyword Automatic debugging ♦ Incorrectness ♦ Termination ♦ Correctness ♦ Logical analysis ♦ Invariants ♦ Program verification
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.
Description Affiliation: IBM Research Center, Technion, Haifa, Israel (Katz, Shmuel; Manna, Zohar)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2005-08-01
Publisher Place New York
Journal Communications of the ACM (CACM)
Volume Number 19
Issue Number 4
Page Count 19
Starting Page 188
Ending Page 206

Open content in new tab

   Open content in new tab
Source: ACM Digital Library