zbMATH — the first resource for mathematics

More precise yet widely applicable cost analysis. (English) Zbl 1317.68027
Jhala, Ranjit (ed.) et al., Verification, model checking, and abstract interpretation. 12th international conference, VMCAI 2011, Austin, TX, USA, January 23–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-18274-7/pbk). Lecture Notes in Computer Science 6538, 38-53 (2011).
Summary: Cost analysis aims at determining the amount of resources required to run a program in terms of its input data sizes. Automatically inferring precise bounds, while at the same time being able to handle a wide class of programs, is a main challenge in cost analysis. (1) Existing methods which rely on computer algebra systems (CAS) to solve the obtained cost recurrence equations (CR) are very precise when applicable, but handle a very restricted class of CR. (2) Specific solvers developed for CR tend to sacrifice accuracy for wider applicability. In this paper, we present a novel approach to inferring precise upper and lower bounds on CR which, when compared to (1), is strictly more widely applicable while precision is kept and when compared to (2), is in practice more precise (obtaining even tighter complexity orders), keeps wide applicability and, besides, can be applied to obtain useful lower bounds as well. The main novelty is that we are able to accurately bound the worst-case/best-case cost of each iteration of the program loops and, then, by summing the resulting sequences, we achieve very precise upper/lower bounds.
For the entire collection see [Zbl 1206.68013].

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Full Text: DOI
[1] Albert, E., Arenas, P., Genaim, S., Herraiz, I., Puebla, G.: Comparing cost functions in resource analysis. In: van Eekelen, M., Shkaravska, O. (eds.) FOPARA 2009. LNCS, vol. 6324, pp. 1–17. Springer, Heidelberg (2010) · Zbl 1305.68051 · doi:10.1007/978-3-642-15331-0_1
[2] Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-Form Upper Bounds in Static Cost Analysis. Journal of Automated Reasoning (to appear, 2010) · Zbl 1213.68200
[3] Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost Analysis of Java Bytecode. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 157–172. Springer, Heidelberg (2007) · Zbl 05187152 · doi:10.1007/978-3-540-71316-6_12
[4] Bagnara, R., Pescetti, A., Zaccagnini, A., Zaffanella, E.: PURRS: Towards Computer Algebra Support for Fully Automatic Worst-Case Complexity Analysis. Technical report (2005), arXiv:cs/0512056, http://arxiv.org/
[5] Ben-Amram, A.M.: Size-change termination, monotonicity constraints and ranking functions. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 109–123. Springer, Heidelberg (2009) · Zbl 1242.68061 · doi:10.1007/978-3-642-02658-4_12
[6] Feautrier, P., Alias, C., Darte, A., 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
[7] Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. POPL. ACM, New York (1978)
[8] Crary, K., Weirich, S.: Resource bound certification. In: POPL 2000. ACM Press, New York (2000) · Zbl 1323.68368
[9] Gulwani, S., Mehra, K.K., Chilimbi, T.M.: Speed: precise and efficient static estimation of program computational complexity. In: POPL, pp. 127–139. ACM, New York (2009) · Zbl 1315.68095
[10] Hoffmann, J., Hofmann, M.: Amortized resource analysis with polynomial potential. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 287–306. Springer, Heidelberg (2010) · Zbl 1260.68074 · doi:10.1007/978-3-642-11957-6_16
[11] Marriot, K., Stuckey, P.: Programming with Constraints: An Introduction. The MIT Press, Cambridge (1998)
[12] Maxima.sourceforge.net. Maxima, a Computer Algebra System. Version 5.21.1 (2009), http://maxima.sourceforge.net/
[13] Wegbreit, B.: Mechanical Program Analysis. Communications of the ACM 18(9) (1975) · Zbl 0306.68008 · doi:10.1145/361002.361016
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.