Interpolant-Based Transition Relation Approximation

Details Interpolant-Based Transition Relation Approximation Interpolant-Based Transition Relation Approximation

2007-06-04

arxiv.org/abs/0706.0523v2

LMCS 3 (4:1) 2007

Computer Science

Logic in Computer Science

Conference Version at CAV 2005. 17 Pages, 9 Figures

Scientific paper

10.2168/LMCS-3(4:1)2007

In predicate abstraction, exact image computation is problematic, requiring in the worst case an exponential number of calls to a decision procedure. For this reason, software model checkers typically use a weak approximation of the image. This can result in a failure to prove a property, even given an adequate set of predicates. We present an interpolant-based method for strengthening the abstract transition relation in case of such failures. This approach guarantees convergence given an adequate set of predicates, without requiring an exact image computation. We show empirically that the method converges more rapidly than an earlier method based on counterexample analysis.

Affiliated with

Also associated with

No associations

Rating

Interpolant-Based Transition Relation Approximation does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Interpolant-Based Transition Relation Approximation, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Interpolant-Based Transition Relation Approximation will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-121199