Computer Science – Software Engineering
Scientific paper
2012-01-24
Computer Science
Software Engineering
19 pages
Scientific paper
This article focuses on automatically generating polynomial equations that are inductive loop invariants of computer programs. We propose a new algorithm for this task, which is based on polynomial interpolation. Though the proposed algorithm is not complete, it is efficient and can be applied to a broader range of problems compared to existing methods targeting similar problems. The efficiency of our approach is testified by experiments on a large collection of programs. The current implementation of our method is based on dense interpolation, for which a total degree bound is needed. On the theoretical front, we study the degree and dimension of the invariant ideal of loops which have no branches and where the assignments define a P-solvable recurrence. In addition, we obtain sufficient conditions for non-trivial polynomial equation invariants to exist (resp. not to exist).
Maza Marc Moreno
Xiao Rong
No associations
LandOfFree
Generating Program Invariants via Interpolation 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 Generating Program Invariants via Interpolation, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Generating Program Invariants via Interpolation will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-107667