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 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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bornat, R.: Proofs of pointer programs in Jape. available at: http://www.dcs.qmul.ac.uk/richard/pointers/
Bornat, R.: Proving pointer programs in Hoare logic. In: Mathematics of Program Construction, pp. 102–126 (July 2000)
Bornat, R., Sufrin, B.: Animating formal proofs at the surface: The Jape proof calculator. The Computer Journal 43, 177–192 (1999)
Hendren, L.: Parallelizing Programs with Recursive Data Structures. PhD thesis, Dept. of Computer Science, Cornell University (January 1990)
Ishtiaq, S., O’Hearn, P.: Bi as an assertion language for mutable data structures. In: Symp. on Principles of Programming Languages, pp. 14–26 (January 2001)
Knuth, D.: The Art of Computer Programming. Fundamental Algorithms, vol. 1. Addison-Wesley, Reading (1973)
Lee, O., Yang, H., Yi, K.: Automatic verification of pointer programs using grammar-based shape analysis. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 124–140. Springer, Heidelberg (2005)
Lev-Ami, T., Immerman, N., Sagiv, M.: Fast and precise abstraction for shape analysis. In: Proc. Computer-Aided Verification (August 2006) (to appear)
Lev-Ami, T., Reps, T., Sagiv, M., Wilhelm, R.: Putting static analysis to work for verification: A case study. In: Int. Symp. on Software Testing and Analysis, pp. 26–38 (August 2000)
Lindstrom, G.: Scanning list structures without stacks or tag bits. Information Processing Letters 2(2), 47–51 (1973)
Loginov, A., Reps, T., Sagiv, M.: Abstraction refinement via inductive learning. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 519–533. Springer, Heidelberg (2005)
Manevich, R., Sagiv, M., Ramalingam, G., Field, J.: Partially disjunctive heap abstraction. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 265–279. Springer, Heidelberg (2004)
Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. In: Baader, F. (ed.) CADE 2003. LNCS, vol. 2741, pp. 121–135. Springer, Heidelberg (2003)
Morris, J.: Verification-oriented language design. Tech. Report TR-7, Computer Science Div., University of California–Berkeley (December 1972)
Reps, T., Sagiv, M., Loginov, A.: Finite differencing of logical formulas for static analysis. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 380–398. Springer, Heidelberg (2003)
Reynolds, J.: Separation Logic: A logic for shared mutable data structures. In: Symp. on Logic in Computer Science, pp. 55–74 (July 2002)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. on Programming Languages and Systems (TOPLAS) 24(3), 217–298 (2002)
Schorr, H., Waite, W.: An efficient machine independent procedure for garbage collection in various list structures. Communications of the ACM 10(8), 501–506 (1967)
Suzuki, N.: Automatic Verification of Programs with Complex Data Structures. PhD thesis, Dept. of Computer Science, Stanford University (February 1976)
Topor, R.: The correctness of the Schorr-Waite list marking algorithm. Tech. Report MIP-R-104, School of Artificial Intelligence, University of Edinburgh (July 1974)
Yang, H.: Local Reasoning for Stateful Programs. PhD thesis, Dept. of Computer Science, University of Illinois, Urbana-Champaign (June 2001)
Yelowitz, L., Duncan, A.: Abstractions, instantiations, and proofs of marking algorithms. In: Symp. on Artificial Intelligence and Programming Languages, pp. 13–21 (August 1977)
Yorsh, G., Reps, T., Sagiv, M., Wilhelm, R.: Logical characterizations of heap abstractions. ACM Transactions on Computational Logic (TOCL) (to appear)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Loginov, A., Reps, T., Sagiv, M. (2006). Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm. In: Yi, K. (eds) Static Analysis. SAS 2006. Lecture Notes in Computer Science, vol 4134. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11823230_17
Download citation
DOI: https://doi.org/10.1007/11823230_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37756-6
Online ISBN: 978-3-540-37758-0
eBook Packages: Computer ScienceComputer Science (R0)