Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm
Alexey Loginov (University of Wisconsin), Thomas Reps (University of Wisconsin) and Mooly Sagiv (Tel-Aviv University)
Abstract
This paper reports on the automated verification of the total correctness (partial correctness and termination) of the Deutsch-Schorr-Waite (DSW) algorithm. DSW is an algorithm for traversing a binary tree without the use of a stack by means of destructive pointer manipulation. Prior approaches to the verification of the algorithm involved semi-automated applications of theorem provers or hand-written proofs. TVLA's abstract-interpretation approach made possible the automatic symbolic exploration of all memory configurations that can arise. With the introduction of a few simple core and instrumentation relations, TVLA was able to establish the partial correctness and termination of DSW.