×

Runtime complexity analysis of logically constrained rewriting. (English) Zbl 07496640

Fernández, Maribel (ed.), Logic-based program synthesis and transformation. 30th international symposium, LOPSTR 2020, Bologna, Italy, September 7–9, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12561, 37-55 (2021).
Summary: Logically constrained rewrite systems (LCTRSs) are a versatile and efficient rewriting formalism that can be used to model programs from various programming paradigms, as well as simplification systems in compilers and SMT solvers. In this paper, we investigate techniques to analyse the worst-case runtime complexity of LCTRSs. For that, we exploit synergies between previously developed decomposition techniques for standard term rewriting by Avanzini et al. in conjunction with alternating time and size bound approximations for integer programs by Brockschmidt et al. and adapt these techniques suitably to LCTRSs. Furthermore, we provide novel modularization techniques to exploit loop bounds from recurrence equations which yield sublinear bounds. We have implemented the method in \(\mathsf{T_CT}\) to test the viability of our method.
For the entire collection see [Zbl 1482.68019].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

TiML; TcT; KITTeL; Ctrl; Maude; Yices; z3
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Albert, E.; Arenas, P.; Genaim, S.; Puebla, G.; Alpuente, M.; Vidal, G., Automatic inference of upper bounds for recurrence relations in cost analysis, Static Analysis, 221-237 (2008), Heidelberg: Springer, Heidelberg · Zbl 1149.68345 · doi:10.1007/978-3-540-69166-2_15
[2] Albert, E.; Genaim, S.; Masud, AN, On the inference of resource usage upper and lower bounds, ACM TOCL, 14, 3, 22 (2013) · Zbl 1353.68045 · doi:10.1145/2499937.2499943
[3] Avanzini, M., Dal Lago, U., Moser, G.: Analysing the complexity of functional programs: higher-order meets first-order. In: Proceedings of the 20th ICFP, pp. 152-164. ACM (2015). doi:10.1145/2784731.2784753 · Zbl 1360.68313
[4] Avanzini, M.; Moser, G., A combination framework for complexity, Inf. Comput., 248, 22-55 (2016) · Zbl 1339.68135 · doi:10.1016/j.ic.2015.12.007
[5] Avanzini, M.; Moser, G.; Schaper, M.; Chechik, M.; Raskin, J-F, TcT: Tyrolean complexity tool, Tools and Algorithms for the Construction and Analysis of Systems, 407-423 (2016), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-662-49674-9_24
[6] Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998). doi:10.1017/CBO9781139172752 · Zbl 0948.68098
[7] Bagnara, R., Mesnard, F.: Eventual linear ranking functions. In: Proceedings of the 15th PPDP, pp. 229-238 (2013). doi:10.1145/2505879.2505884
[8] Brockschmidt, M.; Emmes, F.; Falke, S.; Fuhs, C.; Giesl, J., Analyzing runtime and size complexity of integer programs, ACM Trans. Program. Lang. Syst., 38, 4, 131-1350 (2016) · doi:10.1145/2866575
[9] Chatterjee, K.; Fu, H.; Goharshady, AK; Majumdar, R.; Kunčak, V., Non-polynomial worst-case analysis of recursive programs, Computer Aided Verification, 41-63 (2017), Cham: Springer, Cham · Zbl 1494.68053 · doi:10.1007/978-3-319-63390-9_3
[10] Ciobâcă, Ş.; Lucanu, D.; Galmiche, D.; Schulz, S.; Sebastiani, R., A coinductive approach to proving reachability properties in logically constrained term rewriting systems, Automated Reasoning, 295-311 (2018), Cham: Springer, Cham · Zbl 1511.68132 · doi:10.1007/978-3-319-94205-6_20
[11] Clavel, M., All About Maude - A High-Performance Logical Framework (2007), Heidelberg: Springer, Heidelberg · Zbl 1115.68046 · doi:10.1007/978-3-540-71999-1
[12] de Moura, L.; Bjørner, N.; Ramakrishnan, CR; Rehof, J., Z3: an efficient SMT solver, Tools and Algorithms for the Construction and Analysis of Systems, 337-340 (2008), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-540-78800-3_24
[13] Debray, S.K., López-García, P., Hermenegildo, M.V., Lin, N.: Lower bound cost estimation for logic programs. In: Proceedings of the 14th ILPS, pp. 291-305 (1997). doi:10.7551/mitpress/4283.003.0035
[14] Dutertre, B.; Biere, A.; Bloem, R., Yices 2.2, Computer Aided Verification, 737-744 (2014), Cham: Springer, Cham · doi:10.1007/978-3-319-08867-9_49
[15] Falke, S., Kapur, D., Sinz, C.: Termination analysis of C programs using compiler intermediate languages. In: Proceedings of the 22nd RTA, Volume 10 of LIPIcs, pp. 41-50 (2011). doi:10.4230/LIPIcs.RTA.2011.41 · Zbl 1236.68040
[16] Flores-Montoya, A.; Fitzgerald, J.; Heitmeyer, C.; Gnesi, S.; Philippou, A., Upper and lower amortized cost bounds of programs expressed as cost relations, FM 2016: Formal Methods, 254-273 (2016), Cham: Springer, Cham · doi:10.1007/978-3-319-48989-6_16
[17] Flores-Montoya, A.: Cost analysis of programs based on the refinement of cost relations. Ph.D. thesis, Universität Darmstadt (2017)
[18] Frohn, F.; Giesl, J.; Polikarpova, N.; Schneider, S., Complexity analysis for Java with AProVE, Integrated Formal Methods, 85-101 (2017), Cham: Springer, Cham · Zbl 1498.68065 · doi:10.1007/978-3-319-66845-1_6
[19] Fuhs, C.; Giesl, J.; Plücker, M.; Schneider-Kamp, P.; Falke, S.; Treinen, R., Proving termination of integer term rewriting, Rewriting Techniques and Applications, 32-47 (2009), Heidelberg: Springer, Heidelberg · Zbl 1242.68131 · doi:10.1007/978-3-642-02348-4_3
[20] Fuhs, C.; Kop, C.; Nishida, N., Verifying procedural programs via constrained rewriting induction, ACM TOCL, 18, 2, 14:1-14:50 (2017) · Zbl 1367.68248 · doi:10.1145/3060143
[21] Furuichi, Y.; Nishida, N.; Sakai, M.; Kusakari, K.; Sakabe, T., Approach to procedural program verification based on implicit induction of constrained term rewriting systems, IPSJ Trans. Inf. Syst., 1, 2, 100-121 (2008)
[22] Giesl, J., Analyzing program termination and complexity automatically with AProVE, J. Autom. Reasoning, 58, 1, 3-31 (2017) · Zbl 1409.68255 · doi:10.1007/s10817-016-9388-y
[23] Giesl, J., Ströder, T., Schneider-Kamp, P., Emmes, F., Fuhs, C.: Symbolic evaluation graphs and term rewriting-a general methodology for analyzing logic programs. In: Proceedings of the 14th PPDP, pp. 1-12. ACM Press (2012). doi:10.1007/978-3-642-38197-3_1
[24] Gulwani, S.; Bouajjani, A.; Maler, O., SPEED: symbolic complexity bound analysis, Computer Aided Verification, 51-62 (2009), Heidelberg: Springer, Heidelberg · Zbl 1242.68121 · doi:10.1007/978-3-642-02658-4_7
[25] Hirokawa, N.; Moser, G.; Armando, A.; Baumgartner, P.; Dowek, G., Automated complexity analysis based on the dependency pair method, Automated Reasoning, 364-379 (2008), Heidelberg: Springer, Heidelberg · Zbl 1165.68390 · doi:10.1007/978-3-540-71070-7_32
[26] Hoffmann, J., Das, A., Weng, S.-C.: Towards automatic resource bound analysis for OCaml. In: Proceedings of the 44th POPL, pp. 359-373. ACM (2017). doi:10.1145/3009837 · Zbl 1380.68123
[27] Kop, C.: Termination of LCTRSs. In: Proceedings of the 13th WST, pp. 59-63 (2013)
[28] Kop, C.; Nishida, N.; Fontaine, P.; Ringeissen, C.; Schmidt, RA, Term rewriting with logical constraints, Frontiers of Combining Systems, 343-358 (2013), Heidelberg: Springer, Heidelberg · Zbl 1398.68276 · doi:10.1007/978-3-642-40885-4_24
[29] Kop, C.; Nishida, N.; Davis, M.; Fehnker, A.; McIver, A.; Voronkov, A., Constrained term rewriting tooL, Logic for Programming, Artificial Intelligence, and Reasoning, 549-557 (2015), Heidelberg: Springer, Heidelberg · Zbl 1471.68110 · doi:10.1007/978-3-662-48899-7_38
[30] Lopes, N.; Menendez, D.; Nagarakatte, S.; Regehr, J., Practical verification of peephole optimizations with Alive, Commun. ACM, 61, 2, 84-91 (2018) · doi:10.1145/3166064
[31] Mesnard, F.; Neumerkel, U.; Cousot, P., Applying static analysis techniques for inferring termination conditions of logic programs, Static Analysis, 93-110 (2001), Heidelberg: Springer, Heidelberg · Zbl 1005.68509 · doi:10.1007/3-540-47764-0_6
[32] Moser, G.; Schaper, M., From Jinja bytecode to term rewriting: a complexity reflecting transformation, Inf. Comput., 261, Part, 116-143 (2018) · Zbl 1395.68160 · doi:10.1016/j.ic.2018.05.007
[33] Nishida, N.; Winkler, S.; Piskac, R.; Rümmer, P., Loop detection by logically constrained term rewriting, Verified Software. Theories, Tools, and Experiments, 309-321 (2018), Cham: Springer, Cham · Zbl 1403.68107 · doi:10.1007/978-3-030-03592-1_18
[34] Noschinski, L.; Emmes, F.; Giesl, J., Analyzing innermost runtime complexity of term rewriting by dependency pairs, J. Autom. Reasoning, 51, 1, 27-56 (2013) · Zbl 1314.68174 · doi:10.1007/s10817-013-9277-6
[35] Podelski, A.; Rybalchenko, A.; Steffen, B.; Levi, G., A complete method for the synthesis of linear ranking functions, Verification, Model Checking, and Abstract Interpretation, 239-251 (2004), Heidelberg: Springer, Heidelberg · Zbl 1202.68109 · doi:10.1007/978-3-540-24622-0_20
[36] Serrano, A.; López-García, P.; Hermenegildo, M., Resource usage analysis of logic programs via abstract interpretation using sized types, TPLP, 14, 4-5, 739-754 (2014) · Zbl 1307.68022 · doi:10.1017/S147106841400057X
[37] TeReSe: Term rewriting systems. In: Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press (2003) · Zbl 1030.68053
[38] Wang, P., Wang, D., Chlipala, A.: TiML: a functional language for practical complexity analysis with invariants. Proc. ACM Program. Lang. 1(OOPSLA) (2017). doi:10.1145/3133903
[39] Wilhelm, R., et al.: The worst-case execution-time problem - overview of methods and survey of tools. ACM Trans. Prog. Lang. Syst. 7(3) (2008). doi:10.1145/1347375.1347389
[40] Wilhelm, R.; Grund, D., Computation takes time, but how much?, Commun. ACM, 57, 2, 94-103 (2014) · doi:10.1145/2500886
[41] Winkler, S., Middeldorp, A.: Completion for logically constrained rewriting. In Proceedings of the 3rd FSCD, Volume 108 of LIPIcs, pp. 30:1-30:18 (2018). doi:10.4230/LIPIcs.FSCD.2018.30 · Zbl 1462.68098
[42] Winkler, S., Moser, G.: Runtime complexity analysis of logically constrained rewriting (extended version). http://cl-informatik.uibk.ac.at/users/swinkler/lctrs_complexity/paper.pdf · Zbl 07496640
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.