Verifying reachability invariants of linked structures

ABSTRACT

The paper introduces a reachability predicate for linear lists, develops the elementary axiomatic theory of the predicate, and illustrates its application to program verification with a formal proof of correctness for a short program that traverses and splices linear lists.

REFERENCES

• 1: Burstall, R. M., "Some techniques for proving correctness of programs which alter data structures", Machine Intelligence 6, pp. 23-50, Edinburgh, Edinburgh University Press, 1971.
• 2: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 3: David C. Luckham , Norihisa Suzuki, Automatic program verification V: verification-oriented proof rules for arrays, records and pointers, Stanford University, Stanford, CA, 1976
• 4: Morris, J. H., "Verification-oriented language design", Technical Report 7, Department of Computer Science, UC Berkeley, December, 1972.
• 5: Nelson, G., "Techniques for program verification", CSL-81-10, Xerox Palo Alto Research Center, June, 1981.
• 6: Nelson, G. and Yao, F., "Solving reachability constraints for linear lists", manuscript, August 1982.