Shape and Content: Incorporating Domain Knowledge into Shape Analysis

Technical Report, arXiv.org e-Print archive. CoRR Technical Report arXiv:1312.6624 2014. Available at https://arxiv.org/abs/1312.6624.

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 attempt to bridge the conceptual gap between these two communities. 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. We show how description logic can be used on top of an existing shape analysis to add content descriptions to the shapes. 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. Thus, we obtain a modular description logic based verification methodology which is able to exploit shape information.

@techreport{arXiv-2014-shape-dls,
   title = "Shape and Content:  Incorporating Domain Knowledge into Shape
Analysis",
   year = "2014",
   author = "Diego Calvanese and Tomer Kotek and Mantas Simkus and
Helmut Veith and Florian Zuleger",
   institution = "arXiv.org e-Print archive",
   number = "arXiv:1312.6624",
   note = "Available at https://arxiv.org/abs/1312.6624",
}