On the Limits of the Classical Approach to Cost Analysis

1. Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-Form Upper Bounds in Static Cost Analysis. Journal of Automated Reasoning 46(2), 161–203 (2011)

   Article  MathSciNet  MATH  Google Scholar 

2. Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost Analysis of Object-Oriented Bytecode Programs. Theoretical Computer Science 413(1), 142–159 (2012)

   Article  MathSciNet  MATH  Google Scholar 

3. Albert, E., Genaim, S., Gómez-Zamalloa, M.: Parametric Inference of Memory Requirements for Garbage Collected Languages. In: ISMM, pp. 121–130. ACM, New York (2010)

   Google Scholar 

4. Albert, E., Genaim, S., Masud, A.N.: More Precise Yet Widely Applicable Cost Analysis. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 38–53. Springer, Heidelberg (2011)

   Chapter  Google Scholar 

5. Anderson, H., Khoo, S.-C., Andrei, Ş., Luca, B.: Calculating Polynomial Runtime Properties. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 230–246. Springer, Heidelberg (2005)

   Chapter  Google Scholar 

6. Benoy, F., King, A.: Inferring Argument Size Relationships with CLP(R). In: Gallagher, J.P. (ed.) LOPSTR 1996. LNCS, vol. 1207, pp. 204–223. Springer, Heidelberg (1997)

   Chapter  Google Scholar 

7. Brown, C.W., Gross, C.: Efficient Preprocessing Methods for Quantifier Elimination. In: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (eds.) CASC 2006. LNCS, vol. 4194, pp. 89–100. Springer, Heidelberg (2006)

   Chapter  Google Scholar 

8. Chen, Y., Xia, B., Yang, L., Zhan, N., Zhou, C.: Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 34–49. Springer, Heidelberg (2007)

   Chapter  Google Scholar 

9. Cormen, T.H., Leiserson, C.E., Rivest, R., Stein, C.: Introduction to Algorithms, 3rd edn. MIT Press (2009)

   Google Scholar 

10. Debray, S.K., Lin, N.-W.: Cost Analysis of Logic Programs. ACM Transactions on Programming Languages and Systems 15(5), 826–875 (1993)

    Article  Google Scholar 

11. Dolzmann, A., Sturm, T.: REDLOG: Computer Algebra meets Computer Logic. ACM SIGSAM Bulletin 31(2), 2–9 (1997)

    Article  MathSciNet  Google Scholar 

12. Gulwani, S., Mehra, K.K., Chilimbi, T.M.: SPEED: Precise and Efficient Static Estimation of Program Computational Complexity. In: Proc. of POPL 2009, pp. 127–139. ACM (2009)

    Google Scholar 

13. Gulwani, S., Zuleger, F.: The Reachability-Bound Problem. In: PLDI, pp. 292–304. ACM (2010)

    Google Scholar 

14. Hickey, T.J., Cohen, J.: Automating Program Analysis. J. ACM 35(1), 185–220 (1988)

    Article  MathSciNet  MATH  Google Scholar 

15. Hofmann, M., Hoffmann, J., Aehlig, K.: Multivariate Amortized Resource Analysis. In: POPL 2011, pp. 357–370. ACM (2011)

    Google Scholar 

16. Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: Deduction and Applications, vol. 05431 (2006)

    Google Scholar 

17. Le Métayer, D.: ACE: An Automatic Complexity Evaluator. ACM Trans. Program. Lang. Syst. 10(2), 248–266 (1988)

    Article  Google Scholar 

18. Monniaux, D.: Automatic modular abstractions for template numerical constraints. Logical Methods in Computer Science 6(3) (2010)

    Google Scholar 

19. Sturm, T., Tiwari, A.: Verification and Synthesis using Real Quantifier Elimination. In: ISSAC 2011, pp. 329–336. ACM (2011)

    Google Scholar 

20. REDUCE Computer Algebra System. REDUCE home page

    Google Scholar 

21. Z3 Theorem Prover. Z3 home page

    Google Scholar 

22. Wegbreit, B.: Mechanical Program Analysis. Communications of the ACM 18(9) (1975)

    Google Scholar 

23. Zuleger, F., Gulwani, S., Sinn, M., Veith, H.: Bound Analysis of Imperative Programs with the Size-Change Abstraction. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 280–297. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

Download references