In previous work we presented the flow framework for verifying complex concurrent data structures using separation logic (SL). The framework enables the decomposition of the overall correctness proof of the data structure into (1) a proof of an abstract template algorithm that captures the underlying synchronization protocol between data structure operations, and (2) a refinement proof of this template to the concrete data structure implementation. In this paper, we investigate the automation of proofs expressed in this framework. We use the give-up template for concurrent dictionaries, and an implementation of this template based on B+ trees as a case study. We detail the challenges in automating the framework and present a revised version geared towards automation in a standard SL-based symbolic execution engine. We have implemented such an engine in the deductive verification tool GRASShopper and used it to mechanize the proof of our case study. Our experience suggests that the flow framework can express simple correctness proofs of complex concurrent data structures and can be automated using off-the-shelf verification tools, requiring only minor extensions to standard reasoning engines for SL.