Partial Predicate Abstraction and Counter-Example Guided Refinement

TL;DR

This paper introduces a counter-example guided refinement technique for partial predicate abstraction, combining predicate abstraction and fixpoint approximations to improve model checking of infinite-state systems.

Contribution

It presents a novel approach that distinguishes sources of imprecision and applies targeted refinement, enhancing the effectiveness of partial predicate abstraction.

Findings

Effective refinement of abstractions using counter-examples

Distinguishing sources of imprecision improves model checking accuracy

Experimental results demonstrate improved verification performance

Abstract

In this paper we present a counter-example guided abstraction and approximation refinement (CEGAAR) technique for {\em partial predicate abstraction}, which combines predicate abstraction and fixpoint approximations for model checking infinite-state systems. The proposed approach incrementally considers growing sets of predicates for abstraction refinement. The novelty of the approach stems from recognizing source of the imprecision: abstraction or approximation. We use Craig interpolation to deal with imprecision due to abstraction. In the case of imprecision due to approximation, we delay application of the approximation. Our experimental results on a variety of models provide insights into effectiveness of partial predicate abstraction as well as refinement techniques in this context.