一种C程序断言的全自动静态验证方法

Full-Automatic Static Assertion Verification for C Programs

在软件程序中插入断言是保证软件质量的一个简单但有效的方法,人们常使用测试的方法检验程序中的断言是否满足,但测试很难保证验证的完备性。本文提出了一种可以保证完备性的全自动静态断言验证方法,其基本思想是基于程序切片符号执行程序的所有执行路径,并证明路径上的所有断言都满足。为了尽量减少符号执行的语句的数量,使用了基于反例的抽象精化方法,从一个粗略的切片标准开始迭代地符号执行一条路径,根据验证的反例自动生成下一次迭代过程中使用的精化的切片标准。包含循环的程序可能具有无穷多条程序执行路径,提出的基于符号执行上下文不变式证明的方法可以证明由于循环导致的无穷多条路径中断言都满足,从而使得验证过程可以终止。实验表明,提出的全自动静态断言验证方法不仅可行,而且验证代价较小,具有较强的实用性。

Inserting assertions into program source codes is a simple but effective way to ensure software quality. One usually checks the assertions through testing, but the testing based verification can＇t guarantee completeness. We present in this paper a full-automatic static verification method for complete assertion verification. The basic ideal behind our method is symbolically executing every execution trace and proving that all the assertions of the trace hold. We only symbolically execute those statements which are relevant to the assertions and use a slicing criterion to judge which one is relevant. In order to lessen the statements to be executed when symbolically executing a trace, we use the ideal of Counter-Example Guided Abstraction Refinement （CEGAR）to generate a refined slicing criterion from counter-examples and use the new slicing criterion to start a new verification iteration for the same trace until a real counter-example trace found or assertions proved to be hold. There are infinite many traces for programs with loops. We also present a method based on symbolic execution context invariant proving to prove that all assertions of the infinite many traces leading by loops are satisfied and thus make our verification process terminate. It＇s shown by the experiments that the assertion verification method presented in this paper not only is feasible but also has little verification cost.