Shape and Content: Incorporating Domain Knowledge into Shape Analysis
MetadataShow full item record
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 Logics (DLs), a widely used knowledge representation paradigm which gives a logical underpinning for diverse modeling frameworks such as UML and ER. We show how DLs 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. We show that the two-variable fragment of first order logic with counting and trees (whose decidability was presented at LICS~2013) can be used as a joint framework to embed suitable DLs and separation logic.
Showing items related by title, author, creator and subject.
How plot shape and spatial arrangement affect plant species richness counts: implications for sampling design and rarefaction analyses Güler B, Jentsch A, Apostolova I, Bartha S, Bloor J, Campetella G, Canullo R, Házi, J, Kreyling J, Pottier J, Szabó G, Terziyska T, Uğurlu E, Wellstein C, Zimmermann Z, Dengler J (Wiley: 12 months, 2016)Questions: How does the spatial configuration of sampling units influence recorded plant species richness values at small spatial scales? What are the consequences of these findings for sampling methodology and rarefaction ...
Pii Y; Borruso L; Brusetti L; Cesco S; Mimmo T (2016)Microorganisms associated with plants have been shown to improve plant growth and yield participating in the biogeochemical cycles of elements in soil. For these reasons, the rhizosphere microbiome is considered one of the ...
Borgo, S; Kutz, O (CEUR-WS.org, 2011)We propose a formal framework to clarify the import of and the relationship among different notions of similarity. The framework, borrowing from the general E-connections approach, allows to use multiple similarity notions ...