|
 |
[06 Mar]P - property to be verifiedS(n) - State in nth iteration Inductive Technique: Assume that property P holds for S(n-1) and try to deduce that it holds for S(n) too. Sometimes it is possible. For example, the "pathological" example given in Willem's paper. Although automatic invariant detection finds this as a very difficult problem, inductive techqniues solve it very easily. On the other hand, many times it is not possible, especially when we have heap and array updates. This is because, besides P there may be other properties that hold for S(n-1) and which we need to know to deduce that P holds for S(n). So if we are using a theorem prover for our deduction, sometimes it may discover Q and try to prove that Q also holds. But in many cases it does not, and there the user has specify the Q. Above does not make a lot sense! Shape Analysis: I have to read more about it. But the basic idea is to, find out the closed form for the program state S(n) through iterating over the loop until fixedpoint. Then verification of P becomes checking that P holds for the closed form of S(n). Willem's Technique: His technique is based on Hoare style verification, which needs a loop invariant. He tries to find the loop invariant automatically with an iterative algorithm. Novelity of his technique is he uses P to guess the initial candidate invariant. Then it does an iterative strengthening, approximation and refining of the candidate invariants until it finds the actual invariant. Last modified 11 March 2005 at 11:22 am by Saswat Anand |