Experimenting with Predicate Abstraction
Beatriz Sousa Santos, Cláudio Belo Lourenço, Maria João Frade, Jorge Sousa Pinto, João Cachopo, Victor Cacciari Miraldo · 2013
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 existential abstraction of a program, and we establish a common framework for both this direct technique and a second one, based on cartesian abstraction 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 Joao Frade