Automated Theorem Prover for Pointer Logic
Zhenming Wang, Yiyun Chen, Zhi-Fang WANG · Journal of Software · 2009
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.