Abstract
We show how to underapproximate the procedure summaries of recursive programs over the integers using off-the-shelf analyzers for non-recursive programs. The novelty of our approach is that the non-recursive program we compute may capture unboundedly many behaviors of the original recursive program for which stack usage cannot be bounded. Moreover, we identify a class of recursive programs on which our method terminates and returns the precise summary relations without underapproximation. Doing so, we generalize a similar result for non-recursive programs to the recursive case. Finally, we present experimental results of an implementation of our method applied on a number of examples.
Supported by the French National Project ANR-09-SEGI-016 VERIDYC, the Spanish Ministry of Economy and Finance grant (tin2010-20639), and the Rich Model Toolkit initiative.
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
Termination Competition 2011, http://termcomp.uibk.ac.at/termcomp/home.seam
Albarghouthi, A., Gurfinkel, A., Chechik, M.: Whale: An Interpolation-Based Algorithm for Inter-procedural Verification. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 39–55. Springer, Heidelberg (2012)
Alur, R., Madhusudan, P.: Adding nesting structure to words. JACM 56(3), 16 (2009)
Atig, M.F., Ganty, P.: Approximating petri net reachability along context-free traces. In: FSTTCS 2011. LIPIcs, vol. 13, pp. 152–163. Schloss Dagstuhl (2011)
Cook, B., Podelski, A., Rybalchenko, A.: Summarization for termination: no return! Formal Methods in System Design 35, 369–387 (2009)
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., Lakhnech, Y.: Flat parametric counter automata. Fundamenta Informaticae 91(2), 275–303 (2009)
Cowles, J.: Knuth’s generalization of McCarthy’s 91 function. In: Computer-aided Reasoning, pp. 283–299 (2000)
Esparza, J., Kiefer, S., Luttenberger, M.: Newtonian program analysis. JACM 57(6), 33:1–33:47 (2010)
Ganty, P., Iosif, R., Konečný, F.: Underapproximation of procedure summaries for integer programs. CoRR abs/1210.4289 (2012)
Ginsburg, S.: The Mathematical Theory of Context-Free Languages. McGraw-Hill, Inc., New York (1966)
Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.: Compositional may-must program analysis: unleashing the power of alternation. In: POPL 2010, pp. 43–56. ACM (2010)
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)
Gruska, J.: A few remarks on the index of context-free grammars and languages. Information and Control 19(3), 216–223 (1971)
Hojjat, H., Konečný, F., Garnier, F., Iosif, R., Kuncak, V., Rümmer, P.: A Verification Toolkit for Numerical Transition Systems - Tool Paper. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 247–251. Springer, Heidelberg (2012)
Lalire, G., Argoud, M., Jeannet, B.: Interproc., http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/interproc/index.html
Luker, M.: A family of languages having only finite-index grammars. Information and Control 39(1), 14–18 (1978)
Luker, M.: Control sets on grammars using depth-first derivations. Mathematical Systems Theory 13, 349–359 (1980)
Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: POPL 1995, pp. 49–61. ACM (1995)
Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications, ch. 7, pp. 189–233. Prentice-Hall, Inc. (1981)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ganty, P., Iosif, R., Konečný, F. (2013). Underapproximation of Procedure Summaries for Integer Programs. In: Piterman, N., Smolka, S.A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2013. Lecture Notes in Computer Science, vol 7795. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36742-7_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-36742-7_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-36741-0
Online ISBN: 978-3-642-36742-7
eBook Packages: Computer ScienceComputer Science (R0)