%0 Journal Article
%T 一种基于变量可达向量的链表抽象方法
%A 李仁见？
%A 刘万伟？
%A 陈立前？
%A 王戟？
%J 软件学报
%P 1935-1949
%D 2012
%R 10.3724/SP.J.1001.2012.04132
%X 提出了一种链表抽象表示方法.该方法隐式存储链表结点之间的边信息,并采用了一种紧致的链表状态表示,存储开销较低,且维护了链表长度信息,精确度较高.具体而言,根据变量对链表结点的可达性质定义了变量可达向量,采用带计数的变量可达向量集描述链表的形态及数量性质,并定义了基本链表操作的抽象语义.通过简单扩展,该方法可以建模包括环形链表在内的所有单向链表.最后,为了验证该链表抽象方法的正确性,在符号执行框架中进行实验,并对常见链表操作程序的运行时错误、长度相关性质等关键性质进行了分析与验证.
%K 链表抽象方法
%K 符号执行
%K 链表操作程序
%K 变量可达向量
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=4132&flag=1