%0 Journal Article
%T 一种c程序断言的全自动静态验证方法
%A 易晓东 杨学军？
%J 计算机科学
%D 2006
%X 在软件程序中插入断言是保证软件质量的一个简单但有效的方法，人们常使用测试的方法检验程序中的断言是否满足，但测试很难保证验证的完备性。本文提出了一种可以保证完备性的全自动静态断言验证方法，其基本思想是基于程序切片符号执行程序的所有执行路径，并证明路径上的所有断言都满足。为了尽量减少符号执行的语句的数量，使用了基于反例的抽象精化方法，从一个粗略的切片标准开始迭代地符号执行一爷路径，根据验证的反例自动生成下一次迭代过程中使用的精化的切片标准。包含循环的程序可能具有无穷多条程序执行路径，提出的基于符号执行上下文不
%K 断言验证基于程序切片的符号执行基于反例的抽象精化静态分析
%U http://www.jsjkx.com/jsjkx/ch/reader/view_abstract.aspx?file_no=22771226&flag=1