Experimenting with Predicate Abstraction

Abstract

Predicate abstraction is a technique employed in software model checking to produce abstract models that can be conservatively checked for property violations in reasonable time. The precision degree of different abstractions of the same program may differ based on (i) the set of predicates used; or (ii) the algorithmic technique employed to generate the model. In this report we explain how we have extended the implementation of one such technique, that produces the most precise ex- istential abstraction of a program, and we establish a common framework for both this direct technique and a second one, based on cartesian ab- straction by weakest precondition calculations. This report a product of the research grant BI22012 PTDC/EIA-CCO/117590/2010 UMINHO, in the scope of the AVIACC project, supervised by Professors Jorge Sousa Pinto and Maria João Frade.