Automated Verification of Monotonic Data Structure Traversals in C