Invariant Synthesis for Programs Manipulating Lists with Unbounded Data