English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Open

Automatic verification of array manipulating programs is a challengingproblem because it often amounts to the inference of in ductive quantified loopinvariants which, in some cases, may not even be firstorder expressible. Inthis paper, we suggest a novel verification tech nique that is based oninduction on userdefined rank of program states as an alternative toloopinvariants. Our technique, dubbed inductive rank reduction, works in twosteps. Firstly, we simplify the verification problem and prove that the programis correct when the input state con tains an input array of length B or less,using the length of the array as the rank of the state. Secondly, we employ asqueezing function g which converts a program state sigma with an array oflength > B to a state g(sigma) containing an array of length minus 1 or less.We prove that when g satisfies certain natural conditions then if the programviolates its specification on sigma then it does so also on g(sigma). Thecorrectness of the program on inputs with arrays of arbitrary lengths followsby induction. We make our technique automatic for array programs whose lengthof execution is proportional to the length of the input arrays by (i) performing the first step using symbolic execution, (ii) verifying the conditionsrequired of g using Z3, and (iii) providing a heuristic procedure for synthesizing g. We implemented our technique and applied it successfully toseveral interesting arraymanipulating programs, including a bidirec tionalsummation program whose loop invariant cannot be expressed in firstorder logicwhile its specification is quantifier free.

Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction