Verification of mutable linear data structures and iterator-based algorithms in Dafny. - Jorge Blázquez; Manuel Montenegro; Clara Segura (J. Log. Algebraic Methods Program., 2023)