Proof Strategy for Automated Sisal Program Verification

Abstract

The Sisal programming environment which is being developed in IIS also includes a verification module. The previously developed C-light verification system serves as its base, since the C language representations of Sisal programs are actually processed. At the moment we concentrate our efforts on verification of Sisal loop expressions which are translated into the C for-loops. Trying to avoid the well-known problem of the loop invariants we apply a symbolic method of definite iterations. This technique expresses the loop effect in symbolic form. However, the Sisal loop expressions sometimes lead to peculiar C loops. The symbolic forms of such loops in verification conditions are too complex to be proved automatically. In this paper we represent a proof strategy for such formulas. Our strategy introduces logical formula transformations which, in general, do not maintain equivalence. However, the truth of resulting formula guarantees truth of the original one. We proved the soundness of this strategy. We also describe here a verification example.