Abstract Counterexamples for Non-disjunctive Abstractions

Counterexamples for Non-disjunctive ions K. L. McMillan1 and L. D. Zuck2 1 Cadence Research Labs 2 University of Illinois at Chicago Counterexample-guided abstraction refinement (CEGAR) is tant method for tuning abstractions to properties to be verified. The method is commonly used, for example in selecting predicates for e abstraction. To date, however, it has been applied primarily to abstractions, which allow one to speak of an abstract transition nd abstract states. Here, we describe a general framework for CEGAR in non-disjunctive abstractions by introducing a generalized notion of abstract counterexample, and methods for computing such counles. We apply this framework to Indexed Predicate Abstraction (IPA), a promising technique for synthesizing quantified inductive invariants of infinite-state systems. In principle, it can be applied to other unctive abstractions occurring in program analysis.

• Type: Conference
• Year: 2009
• Where: RP
• Authors: Kenneth L. McMillan, Lenore D. Zuck
• Keywords: Abstractions, Cadence Research Labs, Counterexample-guided Abstraction Refinement, RP 2009