DATA STRUCTURE VERIFICATION

摘要

A key component of a program verifier intended to check the memory safety of programs, in the context of pointers and explicit deallocation, is its language for describing data structures. This paper presents a methodology for specifying various global shape properties of data structures, using local specifications in the form of axioms involving arbitrary predicates on scalar fields and pointer equalities. A decision procedure for this class of axioms is then discussed, emphasizing on the matching problem in dealing with the universally quantified assumptions. Since the Pointer Assertion Logic Engine (PALE) is considered the most expressive specification language with a decidable verification problem, the paper includes a comparison between the two approaches, from the viewpoints of expressiveness and performance.