Abstraction and abstract interpretation are key tools for automatically verifying properties of systems. One of the major challenges in abstract interpretation is how to obtain abstractions that are precise enough to provide useful information, and yet abstract enough to allow efficient computation. A related challenge is how to conservatively extract useful information from an abstract value. This is a survey paper on a parametric abstract domain called canonical abstraction, which was motivated by the problem of shape analysis — i.e., the problem of determining "shape invariants" for programs that perform destructive updating on dynamically allocated storage. We discuss three conservative methods from extracting information from abstract values: the first method is obtained using the Kleene interpretation of the query formula; this method is simple and very efficient, but is not very precise. The second method is the most precise, but requires the use of a theorem prover. The third method achieves precision close to the second method with tolerable costs, but requires some additional information from the designers of the abstraction. We discuss the canonical-abstraction domain, and show the properties of programs that have been verified by the domain.
展开▼
