Towards Using Description Logics for Symbolic Shape Analysis

摘要: We investigate description logics as a framework for symbolic shape analysis. propose predicate abstraction based analysis, parameterized by DL to represent the predicates. Depending on chosen logic, sharing, reachability and separation in pointer data structures are expressible. Our work follows trend analysis encoding properties of programs logical formulae [1, 2, 3]. Description with functional atomic roles (for modeling fields), nominals program variables) fixed points natural expressive languages specifying programs, e. g., x doubly linked list, y binary tree (i. e., DAG without sharing), or heap cells reachable from resp. separated. predicates, which concept expressions. The relies reasoners checking subsumption w. r. t. nonempty TBoxes finite models. Ideally, should be complete DL, even decide it. However, if there no such (e. is none handling µALCO 1 f , logic needed express separation) allows trade precision complexity: queries may approximated relaxing functionality restrictions) less but computationally more feasible DLs.