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.
Menu