Title :
A theorem prover for verifying iterative programs over integers
Author :
Sarkar, D. ; De Sarkar, S.C.
Author_Institution :
Dept. of Comput. Sci. & Eng., Indian Inst. of Technol., Kharagpur, India
fDate :
12/1/1989 12:00:00 AM
Abstract :
An implementation of a rule-based theorem prover for verifying iterative programs over integers is presented. The authors emphasize the overall proof construction strategy of the prover which has been able to construct the correctness proofs of all iterative programs taken from the literature. Two performance measures for the prover are proposed, and its proof construction for an array-sorting program is evaluated using these measures
Keywords :
expert systems; iterative methods; program verification; theorem proving; array-sorting program; correctness proofs; iterative programs; overall proof construction strategy; performance measures; rule-based theorem prover; Computer science; Humans; Programmable logic arrays; Sorting;
Journal_Title :
Software Engineering, IEEE Transactions on
