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