基于证据自动机的软件回归验证

Software regression verification based on witness automata

为了在多版本程序验证中利用邻近版本之间的共享信息,提取并重用之前版本证据自动机中的循环不变式,提出基于证据自动机的软件回归验证。首先通过证据预处理生成适用于新版程序的证据文件,然后在辅助不变式增强的k-归纳方法的基础上实现了检验新证据文件及验证新版程序的回归验证过程,最后通过对比实验比较了不使用不变式信息的直接验证与结合或不结合数据流分析的三种回归验证的验证性能。与直接验证相比,不结合与结合数据流分析的回归验证的验证耗时分别减少了49%与75%,而内存消耗分别减少了18%与50%。实验结果表明,当程序满足其验证属性时,基于证据自动机的回归验证能极大地提高验证效率,而将证据自动机与数据流分析相结合的验证方式能得到更好的验证效果。

In order to utilize the shared information between adjacent versions in multi-version program verification,and extract and reuse loop invariants in the witness automaton belonging to the previous version,a software regression verification based on witness automata was proposed.Firstly,the witness file applicable to the new version of programs was generated by witness preprocessing.Then,based on the auxiliary-invariant-enhanced k-induction,the regression verification process was implemented to validate the new witness file and verify the new version of programs.Finally,performance of three kinds of regression verification was compared by contrast experiments,including the so-called“direct”verification that did not use invariant information and verification methods combined with or without data flow analysis.Compared with the direct verification,the time consumption of the regression verification combined with or without data flow analysis was reduced by 49%and 75%respectively,and the memory consumption was reduced by 18%and 50%respectively.The results show that when the program satisfies its verification specification,the regression verification based on witness automata can greatly improve verification efficiency,and the regression method combined with data flow analysis can make it even better.