Abstract
We study programs with integer data, procedure calls and arbitrary call graphs. We show that, whenever the guards and updates are given by octagonal relations, the reachability problem along control flow paths within some language \(w_1^* \ldots w_d^*\) over program statements is decidable in Nexptime. To achieve this upper bound, we combine a program transformation into the same class of programs but without procedures, with an Np-completeness result for the reachability problem of procedure-less programs. Besides the program, the expression \(w_1^* \ldots w_d^*\) is also mapped onto an expression of a similar form but this time over the transformed program statements. Several arguments involving context-free grammars and their generative process enable us to give tight bounds on the size of the resulting expression. The currently existing gap between Np-hard and Nexptime can be closed to Np-complete when a certain parameter of the analysis is assumed to be constant.
P. Ganty—Supported by the EU FP7 2007–2013 program under agreement 610686 POLCA and from the Madrid Regional Government under CM project S2013/ICE-2731 (N-Greens).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The precise definition and use of ranks will be explained in Sect. 4.
- 2.
A relation \(\mathord {\leadsto } \subseteq {\left\{ 1,\ldots ,{\vert {w}\vert } \right\} } \times {\left\{ 1,\ldots ,{\vert {w}\vert } \right\} }\) is said to be nested [2] when no two pairs \(i \leadsto j\) and \(i' \leadsto j'\) cross each other, as in \(i < i' \leqslant j < j'\).
- 3.
Octagonal relations are closed under intersections and compositions [20].
- 4.
Because \(L_{X_i}(G^\cap ) \subseteq L_{X_i}^{(K)}(G^\cap ) \subseteq \bigcup _{j=1}^{m_i} \hat{L}_{X_i}(\varGamma _{i, j} \cap \varGamma _{X_i}^{\scriptscriptstyle \mathbf {df}(K+1)}, G^\cap ) \subseteq L_{X_i}(G^\cap )\) .
References
Abdulla, P.A., Atig, M.F., Delzanno, G., Podelski, A.: Push-down automata with gap-order constraints. In: Arbab, F., Sirjani, M. (eds.) FSEN 2013. LNCS, vol. 8161, pp. 199–216. Springer, Heidelberg (2013)
Alur, R., Madhusudan, P.: Adding nesting structure to words. J. ACM 56(3), 16:1–16:43 (2009)
Atig, M.F., Ganty, P.: Approximating petri net reachability along context-free traces. In: FSTTCS 2011, vol. 13. LIPIcs, pp. 152–163. Schloss Dagstuhl (2011)
Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: Fast: fast acceleration of symbolic transition systems. In: Hunt Jr, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 118–121. Springer, Heidelberg (2003)
Bozga, M., Iosif, R., Konečný, F.: Fast acceleration of ultimately periodic relations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 227–242. Springer, Heidelberg (2010)
Bozga, M., Iosif, R., Konečný, F.: Safety problems are np-complete for flat integer programs with octagonal loops. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 242–261. Springer, Heidelberg (2014)
Bozzelli, L., Pinchinat, S.: Verification of gap-order constraint abstractions of counter systems. Theo. Comput. Sci. 523, 1–36 (2014)
Demri, S., Dhar, A.K., Sangnier, A.: Taming past ltl and flat counter systems. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 179–193. Springer, Heidelberg (2012)
Esparza, J., Ganty, P.: Complexity of pattern-based verification for multithreaded programs. In: POPL 2011, pp. 499–510. ACM Press (2011)
Ganty, P., Iosif, R.: Interprocedural reachability for flat integer programs. CoRR, abs/1405.3069v3 (2015)
Ganty, P., Iosif, R., Konečný, F.: Underapproximation of procedure summaries for integer programs. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 245–259. Springer, Heidelberg (2013)
Ginsburg, S.: The Mathematical Theory of Context-Free Languages. McGraw-Hill Inc., New York (1966)
Godoy, G., Tiwari, A.: Invariant checking for programs with procedure calls. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 326–342. Springer, Heidelberg (2009)
Hojjat, H., Iosif, R., Konečný, F., Kuncak, V., Rümmer, P.: Accelerating interpolants. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 187–202. Springer, Heidelberg (2012)
Kroening, D., Lewis, M., Weissenbacher, G.: Under-approximating loops in c programs for fast counterexample detection. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 381–396. Springer, Heidelberg (2013)
Lazic, R.: The reachability problem for vector addition systems with a stack is not elementary. In: RP 2012 (2012)
Lazic, R., Schmitz, S.: Non-elementary complexities for branching VASS, MELL, and extensions. In: CSL-LICS 2014. ACM (2014)
Luker, M.: A family of languages having only finite-index grammars. Inf. Control 39(1), 14–18 (1978)
Luker, M.: Control sets on grammars using depth-first derivations. Math. Syst. Theo. 13, 349–359 (1980)
Miné, A.: The octagon abstract domain. Higher-Order Symbolic Comput. 19(1), 31–100 (2006)
Minsky, M.: Computation: Finite and Infinite Machines. Prentice-Hall, Upper Saddle River (1967)
Revesz, P.Z.: A closed-form evaluation for datalog queries with integer (gap)-order constraints. Theo. Comput. Sci. 116(1), 117–149 (1993)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Ganty, P., Iosif, R. (2015). Interprocedural Reachability for Flat Integer Programs. In: Kosowski, A., Walukiewicz, I. (eds) Fundamentals of Computation Theory. FCT 2015. Lecture Notes in Computer Science(), vol 9210. Springer, Cham. https://doi.org/10.1007/978-3-319-22177-9_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-22177-9_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-22176-2
Online ISBN: 978-3-319-22177-9
eBook Packages: Computer ScienceComputer Science (R0)