Abstract
In this chapter, we discuss the relational string verification techniques based on multi-track automata. We present an approach that is capable of verifying properties that depend on relations among string variables. We discuss the basic word equations (over string concatenations) and the corresponding automata constructions. We present a verification technique based on forward symbolic reachability analysis with multi-track automata, conservative approximations of word equations and function summarization.
This is a preview of subscription content, log in via an institution to check access.
References
Constantinos Bartzis and Tevfik Bultan. Widening arithmetic automata. In R. Alur and D. Peled, editors, Proceedings of the 16th International Conference on Computer Aided Verification (CAV 2004), volume 3114 of Lecture Notes in Computer Science, pages 321–333. Springer-Verlag, July 2004.
Ahmed Bouajjani, Peter Habermehl, and Tomáš Vojnar. Abstract regular model checking. In Rajeev Alur and Doron A. Peled, editors, Computer Aided Verification: 16th International Conference, CAV 2004, Boston, MA, USA, July 13–17, 2004. Proceedings, pages 372–386, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg.
Fang Yu, Tevfik Bultan, and Oscar H. Ibarra. Relational string verification using multi-track automata. Int. J. Found. Comput. Sci., 22(8):1909–1924, 2011.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this chapter
Cite this chapter
Bultan, T., Yu, F., Alkhalaf, M., Aydin, A. (2017). Relational String Analysis. In: String Analysis for Software Verification and Security. Springer, Cham. https://doi.org/10.1007/978-3-319-68670-7_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-68670-7_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-68668-4
Online ISBN: 978-3-319-68670-7
eBook Packages: Computer ScienceComputer Science (R0)