Abstract
Boolean programs with multiple recursive threads can be captured as pushdown automata with multiple stacks. This model is Turing complete, and hence, one is often interested in analyzing a restricted class which still captures useful behaviors. In this paper, we propose a new class of bounded underapproximations for multi-pushdown systems, which subsumes most existing classes. We develop an efficient algorithm for solving the under-approximate reachability problem, which is based on efficient fix-point computations. We implement it in our tool BHIM and illustrate its applicability by generating a set of relevant benchmarks and examining its performance. As an additional takeaway BHIM solves the binary reachability problem in pushdown automata. To show the versatility of our approach, we then extend our algorithm to the timed setting and provide the first implementation that can handle timed multi-pushdown automata with closed guards.
TCS
Chapter PDF
Similar content being viewed by others
References
Abdulla, P.A., Atig, M.F., Stenman, J.: Dense-timed pushdown automata. In: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012. p. 35–44 (2012), https://doi.org/10.1109/LICS.2012.15
Abdulla, P.A., Atig, M.F., Stenman, J.: The minimal cost reachability problem in priced timed pushdown systems. In: Language and Automata Theory and Applications - 6th International Conference, LATA 2012, A Coruña, Spain, March 5-9, 2012. Proceedings. pp. 58–69 (2012), https://doi.org/10.1007/978-3-642-28332-1_6
Akshay, S., Gastin, P., Jugé, V., Krishna, S.N.: Timed systems through the lens of logic. In: 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019. pp. 1–13 (2019)
Akshay, S., Gastin, P., Krishna, S., Roychowdhury, S.: Revisiting underapproximate reachability for multipushdown systems (2020), https://arxiv.org/abs/2002.05950
Akshay, S., Gastin, P., Krishna, S.N.: Analyzing Timed Systems Using Tree Automata. Logical Methods in Computer Science Volume 14, Issue 2 (May 2018), https://lmcs.episciences.org/4489
Akshay, S., Gastin, P., Krishna, S.N., Sarkar, I.: Towards an efficient tree automata based technique for timed systems. In: 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany. pp. 39:1–39:15 (2017), https://doi.org/10.4230/LIPIcs.CONCUR.2017.39
Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proceedings of the thirty-sixth annual ACM symposium on Theory of computing. pp. 202–211. ACM (2004)
Atig, M.F.: Model-Checking of Ordered Multi-Pushdown Automata. Logical Methods in Computer Science Volume 8, Issue 3 (Sep 2012). https://doi.org/10.2168/LMCS-8(3:20)2012
Bhave, D., Dave, V., Krishna, S.N., Phawade, R., Trivedi, A.: A perfect class of context-sensitive timed languages. In: International Conference on Developments in Language Theory. pp. 38–50. Springer, Berlin, Heidelberg (2016)
Bouajjani, A., Echahed, R., Robbana, R.: On the automatic verification of systems with continuous variables and unbounded discrete data structures. In: International Hybrid Systems Workshop. pp. 64–85. Springer (1994)
Chaki, S., Clarke, E., Kidd, N., Reps, T., Touili, T.: Verifying concurrent message-passing C programs with recursive calls. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. p. 334–349. Springer (2006)
Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to algorithms. MIT press (2009)
Cyriac, A.: Verification of communicating recursive programs via split-width. (Vérification de programmes récursifs et communicants via split-width). Ph.D. thesis, École normale supérieure de Cachan, France (2014), https://tel.archives-ouvertes.fr/tel-01015561
Cyriac, A., Gastin, P., Kumar, K.N.: MSO decidability of multi-pushdown systems via split-width. In: International Conference on Concurrency Theory. pp. 547–561. Springer, Berlin, Heidelberg (2012)
Dang, Z., Ibarra, O.H., Bultan, T., Kemmerer, R.A., Su, J.: Binary reachability analysis of discrete pushdown timed automata. In: International Conference on Computer Aided Verification. p. 69–84. Springer (2000)
Hague, M., Lin, A.W.: Synchronisation- and reversal-bounded analysis of multithreaded programs with counters. In: Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings. p. 260–276 (2012), https://doi.org/10.1007/978-3-642-31424-7_22
Kung, H., Lehman, P.L.: Concurrent manipulation of binary search trees. ACM Transactions on Database Systems (TODS) 5(3), 354–382 (1980)
La Torre, S., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: Logic in Computer Science, 2007. LICS 2007. 22nd Annual IEEE Symposium on. pp. 161–170. IEEE (2007)
La Torre, S., Madhusudan, P., Parlato, G.: The language theory of bounded context-switching. In: Latin American Symposium on Theoretical Informatics. pp. 96–107. Springer (2010)
La Torre, S., Napoli, M.: Reachability of multistack pushdown systems with scope-bounded matching relations. In: International Conference on Concurrency Theory. p. 203–218. Springer (2011)
La Torre, S., Parthasarathy, M., Parlato, G.: Analyzing recursive programs using a fixed-point calculus. ACM Sigplan Notices 44(6), 211–222 (2009)
Madhusudan, P., Parlato, G.: The tree width of auxiliary storage. In: ACM SIGPLAN Notices. vol. 46, pp. 283–294. ACM (2011)
Patin, G., Sighireanu, M., Touili, T.: Spade: Verification of multithreaded dynamic and recursive programs. In: International Conference on Computer Aided Verification. pp. 254–257. Springer (2007)
Qadeer, S.: The case for context-bounded verification of concurrent programs. In: Model Checking Software, 15th International SPIN Workshop, Los Angeles, CA, USA, August 10-12, 2008, Proceedings. pp. 3–6 (2008), https://doi.org/10.1007/978-3-540-85114-1_2
Qadeer, S., Wu, D.: Kiss: keep it simple and sequential. ACM sigplan notices 39(6), 14–24 (2004)
Silberschatz, A., Gagne, G., Galvin, P.B.: Operating system concepts. Wiley (2018)
Torre, S.L., Napoli, M., Parlato, G.: Scope-bounded pushdown languages. International Journal of Foundations of Computer Science 27(02), 215–233 (2016)
Torre, S.L., Parlato, G.: Scope-bounded Multistack Pushdown Systems: Fixed-Point, Sequentialization, and Tree-Width 18, 173–184 (2012). https://doi.org/10.4230/LIPIcs.FSTTCS.2012.173
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Akshay, S., Gastin, P., Krishna, S., Roychowdhury, S. (2020). Revisiting Underapproximate Reachability for Multipushdown Systems. In: Biere, A., Parker, D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. Lecture Notes in Computer Science(), vol 12078. Springer, Cham. https://doi.org/10.1007/978-3-030-45190-5_21
Download citation
DOI: https://doi.org/10.1007/978-3-030-45190-5_21
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45189-9
Online ISBN: 978-3-030-45190-5
eBook Packages: Computer ScienceComputer Science (R0)