  The verification community has studied dynamic data structures primarily in a
bottom-up way by analyzing pointers and the shapes induced by them. Recent work
in fields such as separation logic has made significant progress in extracting
shapes from program source code. Many real world programs however manipulate
complex data whose structure and content is most naturally described by
formalisms from object oriented programming and databases. In this paper, we
look at the verification of programs with dynamic data structures from the
perspective of content representation. Our approach is based on description
logic, a widely used knowledge representation paradigm which gives a logical
underpinning for diverse modeling frameworks such as UML and ER. Technically,
we assume that we have separation logic shape invariants obtained from a shape
analysis tool, and requirements on the program data in terms of description
logic. We show that the two-variable fragment of first order logic with
counting and trees %(whose decidability was proved at LICS 2013) can be used as
a joint framework to embed suitable fragments of description logic and
separation logic.
