A logic and decision procedure for verification of heap-manipulating programs

Heap-manipulating programs (HMPs), which manipulate unbounded linked data structures via pointers, are a major frontier for formal verification of software. Formal verification is the process of proving (or disproving) the correctness of a system with respect to some kind of formal specification or property. The primary contributions of this thesis are the definition of a simple transitive closure logic tailored for formal verification of HMPs, and an efficient decision procedure for this logic. To assess the effectiveness of the proposed approach, we develop an HMP verification framework, which uses our fast implementation of the decision procedure to verify a number of HMP examples. Experimental examples (including three small container functions from the Linux kernel) demonstrate that the logic is practically useful and expressive enough to prove many interesting heap properties. In addition, the decision procedure provides a substantial time and space advantage over previous approaches.Science, Faculty ofComputer Science, Department ofGraduat