Abstract
Verifying correctness of programs operating on data structures has become an integral part of software verification. A method is a program that acts on an input data structure (modeled as a graph) and produces an output data structure. The parameterized correctness problem for such methods can be defined as follows: Given a method and a property of the input graphs, we wish to verify that for all input graphs, parameterized by their size, the output graphs also satisfy the property. We present an automated approach to verify that a given method preserves a given property for a large class of methods. Examples include reversals of linked lists, insertion, deletion and iterative modification of nodes in directed graphs. Our approach draws on machinery from automata theory and temporal logic. For a useful class of data structures and properties, our solution is polynomial in the size of the method and size of the property specification.
This research is supported in part by NSF grants CCR-009-8141 & ITR-CCR-020-5483, and SRC Contract No. 2002-TJ-1026.
Chapter PDF
Similar content being viewed by others
References
Benedikt, M., Reps, T.W., Sagiv, S.: A DecidableLogic for Describing Linked Data Structures. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 2–19. Springer, Heidelberg (1999)
Bouajjani, A., Habermehl, P., Moro, P., Vojnar, T.: Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 13–29. Springer, Heidelberg (2005)
Carton, O.: Chain Automata. In: IFIPWorld Computer Congress, Hamburg, pp. 451–458. Elsevier, North-Holland (1994)
Emerson, E.A., Jutla, C.S.: The Complexity of Tree Automata and Logics of Programs. In: Proceedings of 29th IEEE Foundations of Computer Science, 1988 (FOCS 1988), pp. 328–337 (1988)
Emerson, E.A., Kahlon, V.: Model Checking Large-Scale and Parameterized Resource Allocation Systems. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 251–265. Springer, Heidelberg (2002)
Emerson, E.A., Jutla, C.S.: Tree Automata, Mu-Calculus andDetermi-nacy (Extended Abstract). In: Proceedings of Foundations of Computer Sci-ence (FOCS 1991), pp. 368–377 (1991)
Allen Emerson, E.: Automata, Tableaux, and Temporal Logics. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 79–88. Springer, Heidelberg (1985)
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory. Languages and Computation. Addison-Wesley, Reading (1979)
Lev-Ami, T., Reps, T.W., Sagiv, S., Wilhelm, R.: Putting static analysis to work for verification: A case study. In: International Symposium on Software Testing and Analysis, 2000 (ISSTA 2000), pp. 26–38 (2000)
Møller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: Proceedings of SIGPLAN Conference on Programming Languages Design and Implementation (PLDI 2001), pp. 221–231 (2001)
Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. ACM Transactions on Computational Logic (TOCL), 15(3), 403–435 (2004)
O’Hearn, P., Reynolds, J., Yang, H.: Local Reasoning about Programs that Alter Data Structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)
Reynolds, J.C.: Separation Logic: A Logic for Shared MutableData Structures. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS), pp. 55–74 (2002)
Rosenberg, A.L.: On multi-head finite automata. In: FOCS, pp. 221–228 (1965)
Schnoebelen, P.: The complexity of temporal logic model checking. In: Advances in Modal Logic, papers from 4th International Workshop on Advances in Modal Logic 2002, Toulouse, France, September-October (2002)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Symposium on Principles of Programming Languages, POPL 1999 (1999)
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
Deshmukh, J.V., Emerson, E.A., Gupta, P. (2006). Automatic Verification of Parameterized Data Structures. In: Hermanns, H., Palsberg, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2006. Lecture Notes in Computer Science, vol 3920. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11691372_2
Download citation
DOI: https://doi.org/10.1007/11691372_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33056-1
Online ISBN: 978-3-540-33057-8
eBook Packages: Computer ScienceComputer Science (R0)