Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm

Alexey Loginov, Thomas Reps, and Mooly Sagiv

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 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.

(Click here to access the paper: PDF; (c) Springer-Verlag.)