Refinement-based verification for possibly-cyclic lists

被引：0
作者：
Loginov, Alexey [1 ]
Reps, Thomas [2 ]
Sagiv, Mooly [3 ]
机构：
[1] IBM TJ Watson Res Ctr, Yorktown Hts, NY 10598 USA
[2] Univ Wisconsin, Dept Comp Sci, Madison, WI 53706 USA
[3] Tel Aviv Univ, Sch Comp Sci, IL-69978 Tel Aviv, Israel
来源：
PROGRAM ANALYSIS AND COMPILATION, THEORY AND PRACTICE: ESSAYS DEDICATED TO REINHARD WILHELM ON THE OCCASION OF HIS 60TH BIRTHDAY | 2007年 / 4444卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
In earlier work, we presented an abstraction-refinement mechanism that was successful in verifying automatically the partial correctness of in-situ list reversal when applied to an acyclic linked list [10]. This paper reports on the automatic verification of the total correctness (partial correctness and termination) of the same list-reversal algorithm, when applied to apossibly-cyclic linked list. A key contribution that made this result possible is an extension of the finite differencing technique [14] to enable the maintenance of reachability information for a restricted class of possibly-cyclic data structures, which includes possiblycyclic linked lists.
引用
收藏
页码：247 / +
页数：3
相关论文
共 18 条
  • [1] Distefano D, 2006, LECT NOTES COMPUT SC, V3920, P287
  • [2] Dong GZ, 2000, SIGMOD REC, V29, P44, DOI 10.1145/344788.344808
  • [3] Gotsman A, 2006, LECT NOTES COMPUT SC, V4134, P240
  • [4] HESSE W, 2003, DYNAMIC COMPUTATIONA
  • [5] Immerman N, 2004, LECT NOTES COMPUT SC, V3114, P281
  • [6] IMMERMAN N, 2004, WORKSH COMP SCI LOG, P160
  • [7] KLARLUND N, 1993, SYMP PRINC PROGR LAN
  • [8] LAHIRI SK, 2006, S PRINC PROGR LANG, P115
  • [9] LEE O, 2005, ESOP, P124
  • [10] Loginov A, 2005, LECT NOTES COMPUT SC, V3576, P519
12