Implementation of Pointer Logic for Automated Verification

As the security of software is deeply valued while its complexity and size are increasing, automated verification is highly desirable. On the other hand, verification of pointer programs remains a major challenge. In our previous work pointer logic has been proposed to verify basic safety properties of pointer programs, and in this work, we developed efficient algorithms and techniques to implement pointer logic rules for automated verification. The algorithms and techniques are dedicated to reducing the human effort involved in program verification. Moreover, they have been implemented in a tool -- PLCC to automatically verify a range of non-trivial programs such as basic operations on singly-linked lists, trees, circular doubly-linked list etc. and the experimental results show that in acceptable time pointer logic can be applied to automated verification.