Predicate Abstraction and Canonical Abstraction fo

Authors: Roman Manevich E Yahav G Ramalingam Mooly Sagiv

Publish Date: 2005/1/17

Volume: , Issue: , Pages: 181-198

PDF Link

Abstract

Predicate abstraction and canonical abstraction are two finitary abstractions used to prove properties of programs We study the relationship between these two abstractions by considering a very limited case abstraction of potentially cyclic singlylinked listsWe provide a new and rather precise family of abstractions for potentially cyclic singlylinked lists The main observation behind this family of abstractions is that the number of shared nodes in linked lists can be statically bounded Therefore the number of possible “heap shapes” is also bounded We present the new abstraction in both predicate abstraction form as well as in canonical abstraction formAs we illustrate in the paper given any canonical abstraction it is possible to define a predicate abstraction that is equivalent to the canonical abstraction However with this straightforward simulation the number of predicates used for the predicate abstraction is exponential in the number of predicates used by the canonical abstractionAn important feature of the family of abstractions we present in this paper is that the predicate abstraction representation we define is far more practical as it uses a number of predicates that is quadratic in the number of predicates used by the corresponding canonical abstraction representation In particular for the most abstract abstraction in this family the number of predicates used by the canonical abstraction is linear in the number of program variables while the number of predicates used by the predicate abstraction is quadratic in the number of program variablesWe have encoded this particular predicate abstraction and corresponding transformers in TVLA and used this implementation to successfully verify safety properties of several list manipulating programs including programs that were not previously verified using predicate abstraction or canonical abstraction

Keywords: