The German Research Foundation (DFG) has approved to extend the funding period of the ATTESTOR project for another two-year period. The aim of the follow-up project is to develop novel techniques and tools to support formal reasoning on relational shape properties of (concurrent) pointer programs, allowing e.g. to reason about balanced tree data structures. The overarching goal is to signicantly improve the expressivity, automation, and efficiency of symbolic analysis and verication of such software.