We address the verification of abstract data types (ADTs) implementing associative containers like maps and sets with fine-grained specifications for iterators, which allow for multiple readers and writers in client code. Our verified implementations are written in the verification-aware programming language Dafny. In this paper we introduce new methodological contributions in verifying heap-allocated data structures, such as separation between heap-based components and functional behavior, and fine-grained control of verification proofs. Additionally, we have implemented a library of associative containers in Dafny, including a verified implementation of threaded red-black trees with iterators. These contributions aim to reduce proof complexity in order to improve verification times, while maintaining proper encapsulation.