摘要： 在软件程序中插入断言是保证软件质量的一个简单但有效的方法，人们常使用测试的方法检验程序中的断言是否满足，但测试很难保证验证的完备性。本文提出了一种可以保证完备性的全自动静态断言验证方法，其基本思想是基于程序切片符号执行程序的所有执行路径，并证明路径上的所有断言都满足。为了尽量减少符号执行的语句的数量，使用了基于反例的抽象精化方法，从一个粗略的切片标准开始迭代地符号执行一爷路径，根据验证的反例自动生成下一次迭代过程中使用的精化的切片标准。包含循环的程序可能具有无穷多条程序执行路径，提出的基于符号执行上下文不
易晓东 杨学军. 一种C程序断言的全自动静态验证方法[J]. 计算机科学, 2006, 33(9): 253-256. https://doi.org/
YI Xiao-Dong ,YANG Xue-Jun （College of Computer, National Univ. of Defense Technology, Changsha 410073）. [J]. Computer Science, 2006, 33(9): 253-256. https://doi.org/
首页