Abstract
We address the problem of automatic verification of programs with dynamic data structures. We consider the case of sequential, non-recursive programs manipulating 1-selector-linked structures such as traditional linked lists (possibly sharing their tails) and circular lists. We propose an automata-based approach for a symbolic verification of such programs using the regular model checking framework. Given a program, the configurations of the memory are systematically encoded as words over a suitable finite alphabet, potentially infinite sets of configurations are represented by finite-state automata, and statements of the program are automatically translated into finite-state transducers defining regular relations between configurations. Then, abstract regular model checking techniques are applied in order to automatically check safety properties concerning the shape of the computed configurations or relating the input and output configurations. For this particular purpose, we introduce new techniques for the computation of abstractions of the set of reachable configurations and to refine these abstractions if spurious counterexamples are detected. Finally, we present experimental results showing the applicability of the approach and its efficiency.
This work was supported in part by the French Ministry of Research (ACI project Securité Informatique) and the Czech Grant Agency (projects GA CR 102/04/0780 and 102/03/D211).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abdulla, P.A., d’Orso, J., Jonsson, B., Nilsson, M.: Algorithmic Improvements in Regular Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 236–248. Springer, Heidelberg (2003)
Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract Regular Model Checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 372–386. Springer, Heidelberg (2004)
Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular Model Checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)
Bozga, M., Iosif, R., Lakhnech, Y.: Storeless Semantics and Alias Logic. In: Proc. of PEPM 2003. ACM Press, New York (2003)
Deutsch, A.: Interprocedural May-Alias Analysis for Pointers: Beyond k-Limiting. In: Proc. of PLDI 1994. ACM Press, New York (1994)
Habermehl, P., Vojnar, T.: Regular Model Checking Using Inference of Regular Languages. In: Proc. of the 6th Infinity Workshop (2004)
Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: Verification via Structure Simulation. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 281–294. Springer, Heidelberg (2004)
Jensen, J.L., Jørgensen, M.E., Klarlund, N., Schwartzbach, M.I.: Automatic Verification of Pointer Programs Using Monadic Second-order Logic. In: Proc. of PLDI (1997)
Jonkers, H.B.M.: Abstract Storage Structures. Algorithmic Languages. IFIP (1981)
Jonsson, B., Nilsson, M.: Transitive Closures of Regular Relations for Verifying Infinite-State Systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, p. 220. Springer, Heidelberg (2000)
Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic Model Checking with Rich Assertional Languages. Theoretical Computer Science 256(1–2) (2001)
Klarlund, N., Møller, A.: MONA Version 1.4 User Manual. BRICS, Department of Computer Science. University of Aarhus, Denmark (2001)
Loginov, A., Reps, T., Sagiv, M.: Abstraction Refinement for 3-Valued-Logic Analysis. Technical Report 1504, Computer Science Dept., University of Wisconsin, USA (2004)
Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 181–198. Springer, Heidelberg (2005)
Møller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: Proc. of PLDI 2001. Also in SIGPLAN Notices, vol. 36(5) (May 2001)
Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric Shape Analysis via 3-Valued Logic. TOPLAS 24(3) (2002)
Touili, T.: Widening Techniques for Regular Model Checking. ENTCS 50 (2001)
Venet, A.: Automatic Analysis of Pointer Aliasing for Untyped Programs. Science of Computer Programming 35(2) (1999)
Wolper, P., Boigelot, B.: Verifying Systems with Infinite but Regular State Spaces. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427. Springer, Heidelberg (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bouajjani, A., Habermehl, P., Moro, P., Vojnar, T. (2005). Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. In: Halbwachs, N., Zuck, L.D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2005. Lecture Notes in Computer Science, vol 3440. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31980-1_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-31980-1_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25333-4
Online ISBN: 978-3-540-31980-1
eBook Packages: Computer ScienceComputer Science (R0)