Correctness of Proof Strategy for the Sisal Program Verification
Dmitry Alexandrovich Kondratyev, A. V. Promsky · 2019 International Multi-Conference on Engineering, Computer and Information Sciences (SIBIRCON) · 2019
The Sisal-program verification system is being developed in IIS SB RAS. The experiments show that the proof strategies are very helpful if we aims at automatic verification. Obviously, correctness of such strategies is crucial. We would like to discuss here a strategy which can be applied to verification of definite iterations. This strategy is sequence of formula transformation. Either equivalent formula or more stronger formula is the result of this transformation. Consequently it is enough to prove for each transformation that its result is either equivalent to or stronger than source formula. This proof is a new result presented in this paper.