An Assume Guarantee Approach for Checking Quantified Array Assertions

We present an assume-guarantee method for the verification of quantified array assertions based on a program transformation. A quantified array assertion expresses a property over an array segment such as ”all elements of an array are sorted”. Given a program P n annotated with assertion φ n , our method rewrites P n to either TeX or TeX where TeX is a code fragment. The validity of the assertion is then proven by induction: assuming that φ n − 1 holds for P n − 1 and proving that φ n holds for P n . The program transformation allows to reduce the complexity of the code as well as the assertion to be verified. Experimental results on both text book and real life examples taken from system code show performance improvement compared to our previous approach for checking quantified assertions. Moreover, this new technique enables us to verify challenging programs which are not handled by our previous method and many exiting tools as well.