An Assume Guarantee Approach for Checking Quantified Array Assertions

Mohamed Nassim Seghir

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.
Original languageEnglish
Title of host publicationAlgebraic Methodology and Software Technology
Subtitle of host publication13th International Conference, AMAST 2010, Lac-Beauport, QC, Canada, June 23-25, 2010. Revised Selected Papers
PublisherSpringer Berlin Heidelberg
Pages226-235
Number of pages10
Volume6486
ISBN (Electronic)978-3-642-17796-5
ISBN (Print)978-3-642-17795-8
DOIs
Publication statusPublished - 2010

Cite this