Sciweavers

BIRTHDAY
2006
Springer

Refinement-Based Verification for Possibly-Cyclic Lists

14 years 2 months ago
Refinement-Based Verification for Possibly-Cyclic Lists
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 a possibly-cyclic linked list. A key contribution that made this result possible is an extension of the finitedifferencing technique [14] to enable the maintenance of reachability information for a restricted class of possibly-cyclic data structures, which includes possiblycyclic linked lists.
Alexey Loginov, Thomas W. Reps, Mooly Sagiv
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where BIRTHDAY
Authors Alexey Loginov, Thomas W. Reps, Mooly Sagiv
Comments (0)