Automatic techniques for proving correctness of heap-manipulating programs