Shape analysis attempts to analyze and verify correctness of programs with dynamic data structures. This is a notoriously di cult task, because it necessitates e cient decision procedures for expressive logics on graphs and graph-like structures. In the last decade, model-theoretic approaches have been less prominent, and the leading approach is proof-theoretic [15]. Recent advances in nite model theory have created an opportunity for development of practical modeltheoretic approaches in shape analysis. Description Logics (DLs) are a well established family of logics for Knowledge Representation and Reasoning [2]. They model the domain of interest in terms of concepts (classes of objects) and roles (binary relations between objects). These features make DLs very useful to formally describe and reason about graph-structured information. The usefulness of DLs is witnessed e.g. by the W3C choosing DLs to provide the logical foundations to the standard Web Ontology Language (OWL) [14]. Another application of DLs is formalization and static analysis of UML class diagrams and ER diagrams, which are basic modeling artifacts in object-oriented software development and database design, respectively [4,1]. In these settings, standard reasoning services provided by DLs can be used to verify e.g. the consistency of a diagram. To describe the memory of programs with dynamic data structures using a DL, a rather powerful DL must be chosen. The DL in question needs to allow a computationally problematic combination of constructors: (i) nominals are required to represent the program's variables; (ii) number restrictions are required so that the program's pointers (represented as roles) are interpreted as functions; (iii) inverses are needed for de ning data structures such as trees, where elements in the tree must have at most one parent, and for encoding program computation; and (iv) reachability is required since data structures should contain only elements which are reachable from program variables via program pointers. Our contribution: We introduce and develop decision procedures for the logic ALCQIOb;Re, which extends the closure of ALCQIO under Boolean operations (ALCQIOb) with reachability assertions over nite structures. The main ? The rst, third and fourth author were supported by the Austrian National Research Network S11403-N23 (RiSE) of the Austrian Science Fund (FWF) and by the Vienna Science and Technology Fund (WWTF) through grants PROSEED and ICT12-059. The second author was supported by the FWF project P25518 and the WWTF project ICT12-15.
results of this paper are algorithms which decide the nite satis ability and nite implication problems of ALCQIOb;Re. The algorithms are reductions to nite satis ability in ALCQIO, which suggests relatively simple implementation using existing ALCQIO reasoners. Currently no ALCQIO reasoners over nite structures exist to our knowledge. Still, reasoners over arbitrary structures could be used as part of a program veri cation procedure which is sound but not complete. The algorithms run in NEXPTIME, which is optimal since ALCQIO is already NEXPTIME-hard. We only consider nite structures since only they and not in nite structures can represent the memory of programs.
The reachability assertions guarantee that elements of the universe of a model are reachable in the graph-theoretic sense from initial sets of elements using prescribed sets of binary relation symbols. Alternatively, we can think of ALCQIOb;Re as ALCQIOb interpreted over structures containing an unbounded number of trees of bounded degree d.
ALCQIOb;Re is obtained from ALCQIO by (1) allowing the Boolean connectives _; ^; : and (2) adding two new types of assertions: Reachability Assertion B !S A where A; B 2 NC and S NF. Intuitively, it says that B is contained in A and that A is a set of elements reachable from B, without leaving A, through the roles of S.
Disjointness Assertion Disj(A1; A2) = (A1 u A2 ?) for A1; A2 2 NC. Let RE and DI be sets of reachability respectively disjointness assertions. Compatibility RE and DI compatible if for every B1 !S1 A1 B2 !S2 A2 in RE such that S1 \ S2 6= ;, Disj(A1; A2) is in DI. and If we think of the Ai as the sets of elements in di erent data structures in the memory, then compatibility is the natural statement that that data structures can only share the same domain if they use di erent pointers.
Let denote the re exive-transitive closure, denote role composition, RM = (Ss2S sM \ AM AM) and RM(BM) = fv j 9(u; v) 2 RM: u 2 BMg. We have M j= B !S A i M j= B v A and RM(BM) = AM .
Theorem 1. Let i 2 ALCQIOb;Re for i = 1; 2. There are polynomial-time computable ALCQIO formulas and over an extended vocabulary such that (1) 1 is satis able i is satis able. (2) 1 implies 2 i is not satis able. (3) Satis ability and implication in ALCQIOb;Re is NEXPTIME-complete. Satis ability and implication here are over nite structures.
The proof of Theorem 1 is by reduction to the satis ability problem of ALCQIO. The models of = 1 resp. = 1 ! 2 can be partitioned into standard and non-standard models, depending on whether they satisfy the reachability assertions. Since ALCQIO is contained in rst order logic, ALCQIO cannot express the reachability assertions. However, we can augment so that it is guaranteed that whenever a non-standard model exists, so does a standard model, and the standard model can be obtained from the non-standard model by means of so-called tree surgery. The construction relies on a locality property of ALCQIO.
The logic ALCQIOb;Re is especially suited to shape analysis, since it contains nominals, number restrictions, inverses and reachability. ALCQIOb;Re is strong enough to describe e.g. lists, trees and lists of lists. ALCQIOb;Re supports programs whose data structures have complex sharing patterns, and memory cells (which in model-theoretic terms are elements of the universe of the model) may participate in multiple data structures. The closure of the underlying logic ALCQIOb under Boolean operations allows to describe conditional statements in programs. The decision procedure for implication for ALCQIOb;Re is essential for veri cation applications, since it allows to show that speci cations relating pre- and post-conditions are correct.
Since ALCQIOb;Re is a DL, using ALCQIOb;Re for shape analysis brings
an additional advantage. The veri cation community has focused mostly on
a bottom-up approach to the analysis of programs with dynamic data
structures, which examines pointers and the shapes induced by them. However, many
real world programs manipulate complex data whose structure and content is
most naturally described by formalisms from object oriented programming and
databases such as UML and ER diagrams which are generalized by the
framework of description logic. In another extended abstract in this volume (see also
[
The use of DLs in shape analysis has been previously suggested in [