Tomer Kotek: Shape and Content: A database-theoretic perspective on the analysis of
data structures
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 recent work, 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.
Joint work with Diego Calvanese, Mantas Simkus, Helmut Veith and
Florian Zuleger.