×

zbMATH — the first resource for mathematics

Lower runtime bounds for integer programs. (English) Zbl 06623285
Olivetti, Nicola (ed.) et al., Automated reasoning. 8th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-40228-4/pbk; 978-3-319-40229-1/ebook). Lecture Notes in Computer Science 9706. Lecture Notes in Artificial Intelligence, 550-567 (2016).
Summary: We present a technique to infer lower bounds on the worst-case runtime complexity of integer programs. To this end, we construct symbolic representations of program executions using a framework for iterative, under-approximating program simplification. The core of this simplification is a method for (under-approximating) program acceleration based on recurrence solving and a variation of ranking functions. Afterwards, we deduce asymptotic lower bounds from the resulting simplified programs. We implemented our technique in our tool LoAT and show that it infers non-trivial lower bounds for a large number of examples.
For the entire collection see [Zbl 1337.68016].

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
Apron; Aspic; GitHub; LoAT; PURRS; z3
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Albert, E., Genaim, S., Masud, A.N.: On the inference of resource usage upper and lower bounds. ACM Trans. Comput. Logic 14(3), 22:1–22:35 (2013) · Zbl 1353.68045 · doi:10.1145/2499937.2499943
[2] Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 117–133. Springer, Heidelberg (2010) · Zbl 1306.68017 · doi:10.1007/978-3-642-15769-1_8
[3] Alonso-Blas, D.E., Genaim, S.: On the limits of the classical approach to cost analysis. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 405–421. Springer, Heidelberg (2012) · Zbl 06105917 · doi:10.1007/978-3-642-33125-1_27
[4] Bagnara, R., Pescetti, A., Zaccagnini, A., Zaffanella, E.: \[ {\mathsf PURRS} \] : towards computer algebra support for fully automatic worst-case complexity analysis. CoRR abs/cs/0512056 (2005)
[5] Benchmark examples. https://github.com/s-falke/kittel-koat/tree/master/koat-evaluation/examples
[6] Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 491–504. Springer, Heidelberg (2005) · Zbl 1081.68611 · doi:10.1007/11513988_48
[7] Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 413–429. Springer, Heidelberg (2013) · Zbl 06233050 · doi:10.1007/978-3-642-39799-8_28
[8] Brockschmidt, M., Emmes, F., Falke, S., Fuhs, C., Giesl, J.: Alternating runtime and size complexity analysis of integer programs. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 140–155. Springer, Heidelberg (2014) · Zbl 06400459 · doi:10.1007/978-3-642-54862-8_10
[9] Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: Grove, D., Blackburn, S. (eds.) PLDI 2015, pp. 467–478, ACM (2015) · doi:10.1145/2813885.2737955
[10] de Moura, L., Bjørner, N.S.: \[ \mathsf Z3 \] : an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008) · Zbl 05262379 · doi:10.1007/978-3-540-78800-3_24
[11] Debray, S., López-García, P., Hermenegildo, M.V., Lin, N.: Lower bound cost estimation for logic programs. In: Maluszynski, J. (ed.) ILPS 1997, pp. 291–305. MIT Press (1997)
[12] Falke, S., Kapur, D., Sinz, C.: Termination analysis of imperative programs using bitvector arithmetic. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 261–277. Springer, Heidelberg (2012) · Zbl 06068780 · doi:10.1007/978-3-642-27705-4_21
[13] Farzan, A., Kincaid, Z.: Compositional recurrence analysis. In: Kaivola, R., Wahl, T. (eds.) FMCAD 2015, pp. 57–64. IEEE (2015)
[14] Flores-Montoya, A., Hähnle, R.: Resource analysis of complex programs with cost equations. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 275–295. Springer, Heidelberg (2014) · Zbl 1453.68047 · doi:10.1007/978-3-319-12736-1_15
[15] Frohn, F., Giesl, J., Emmes, F., Ströder, T., Aschermann, C., Hensel, J.: Inferring lower bounds for runtime complexity. In: Fernández, M. (ed.) RTA 2015. LIPIcs, vol. 36, pp. 334–349. Dagstuhl Publishing (2015) · Zbl 1366.68116
[16] Frohn, F., Naaf, M., Hensel, J., Brockschmidt, M., Giesl, J.: Proofs and empirical evaluation of ”Lower Runtime Bounds for Integer Programs” (2016). http://aprove.informatik.rwth-aachen.de/eval/integerLower/ · Zbl 06623285
[17] Gonnord, L., Halbwachs, N.: Combining widening and acceleration in linear relation analysis. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 144–160. Springer, Heidelberg (2006) · Zbl 1225.68071 · doi:10.1007/11823230_10
[18] Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: Dershowitz, N. (ed.) Rewriting Techniques and Applications. LNCS, vol. 355, pp. 167–177. Springer, Heidelberg (1989) · doi:10.1007/3-540-51081-8_107
[19] Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst. 34(3), 14:1–14:62 (2012) · Zbl 1284.68132 · doi:10.1145/2362389.2362393
[20] Jeannet, B., Miné, A.: \[ {\mathsf APRON} \] : a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009) · Zbl 05571933 · doi:10.1007/978-3-642-02658-4_52
[21] Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. ACM SIGPLAN Not. 49(1), 529–540 (2014) · Zbl 1284.68188
[22] Kroening, D., Lewis, M., Weissenbacher, G.: Under-approximating loops in C programs for fast counterexample detection. Form. Meth. Sys. Des. 47(1), 75–92 (2015) · Zbl 1322.68054 · doi:10.1007/s10703-015-0228-1
[23] \[ {\mathsf LoAT} \] . https://github.com/aprove-developers/LoAT
[24] Madhukar, K., Wachter, B., Kroening, D., Lewis, M., Srivas, M.K.: Accelerating invariant generation. In: Kaivola, R., Wahl, T. (eds.) FMCAD 2015, pp. 105–111. IEEE (2015)
[25] Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004) · Zbl 1202.68109 · doi:10.1007/978-3-540-24622-0_20
[26] Sinn, M., Zuleger, F., Veith, H.: A simple and scalable static analysis for bound analysis and amortized complexity analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 745–761. Springer, Heidelberg (2014) · Zbl 06349546 · doi:10.1007/978-3-319-08867-9_50
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.