Sciweavers

Share
RP
2009
Springer

Abstract Counterexamples for Non-disjunctive Abstractions

9 years 6 months ago
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.
Kenneth L. McMillan, Lenore D. Zuck
Added 27 Jul 2010
Updated 27 Jul 2010
Type Conference
Year 2009
Where RP
Authors Kenneth L. McMillan, Lenore D. Zuck
Comments (0)
books