Automated Theorem Prover for Pointer Logic

Abstract: This paper presents a technique for designing theorem prover which mainly based on transformation and substitution for Pointer Logic. The technique realized as a tool called APL is implemented. The APL theorem prover is fully automated with which proofs can be recorded and checked efficiently. The tool is tested on pointer programs mainly about singly-linked lists, doubly-linked lists and binary trees