LARA This is an old revision of the document! Proving Programs with Dynamic Allocation Verification conditions for Insertion into Doubly-Linked List.