Shape and Content: A Database-Theoretic Perspective on the Analysis of Data Structures

Proc. of the 11th Int. Conf. on Integrated Formal Methods (IFM 2014). Volume 8739 of Lecture Notes in Computer Science. 2014.

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 can be used as a joint framework to embed suitable fragments of description logic and separation logic.

@inproceedings{IFM-2014,
   title = "Shape and Content:  A Database-Theoretic Perspective on the
Analysis of Data Structures",
   year = "2014",
   author = "Diego Calvanese and Tomer Kotek and Mantas Simkus and
Helmut Veith and Florian Zuleger",
   booktitle = "Proc. of the 11th Int. Conf. on Integrated Formal Methods
(IFM 2014)",
   pages = "3--17",
   volume = "8739",
   publisher = "Springer",
   series = "Lecture Notes in Computer Science",
   doi = "10.1007/978-3-319-10181-1_1",
}