LARA This is an old revision of the document! Proving Programs with Dynamic Allocation Consider Insertion into Doubly-Linked List. Simplify the program. Compute verification conditions. Simplify (parts of) verification conditions.