SPEED: Symbolic Complexity Bound Analysis

(Invited Talk)
  • Sumit Gulwani
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)


The SPEED project addresses the problem of computing symbolic computational complexity bounds of procedures in terms of their inputs. We discuss some of the challenges that arise and present various orthogonal/complementary techniques recently developed in the SPEED project for addressing these challenges.


Outer Loop Nest Loop Loop Iteration Abstract Domain Program Point 
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.


  1. 1.
    Albert, E., Arenas, P., Genaim, S., Puebla, G.: Automatic inference of upper bounds for recurrence relations in cost analysis. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 221–237. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  2. 2.
    Berdine, J., Chawdhary, A., Cook, B., Distefano, D., O’Hearn, P.: Variance analyses from invariance analyses. In: POPL (2007)Google Scholar
  3. 3.
    Bradley, A., Manna, Z., Sipma, H.: Termination of polynomial programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 113–129. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  4. 4.
    Bradley, A.R., Manna, Z., Sipma, H.B.: The polyranking principle. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1349–1361. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  5. 5.
    Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI, pp. 415–426 (2006)Google Scholar
  6. 6.
    Gulavani, B.S., Gulwani, S.: A numerical abstract domain based on expression abstraction and max operator with application in timing analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 370–384. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  7. 7.
    Gulwani, S., Jain, S., Koskinen, E.: Control-flow refinement and progress invariants for bound analysis. In: PLDI (2009)Google Scholar
  8. 8.
    Gulwani, S., Lev-Ami, T., Sagiv, M.: A combination framework for tracking partition sizes. In: POPL, pp. 239–251 (2009)Google Scholar
  9. 9.
    Gulwani, S., Mehra, K.K., Chilimbi, T.M.: Speed: precise and efficient static estimation of program computational complexity. In: POPL, pp. 127–139 (2009)Google Scholar
  10. 10.
    Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: PLDI, pp. 376–386 (2006)Google Scholar
  11. 11.
    Gustafsson, J., Ermedahl, A., Sandberg, C., Lisper, B.: Automatic derivation of loop bounds and infeasible paths for wcet analysis using abstract execution. In: RTSS, pp. 57–66 (2006)Google Scholar
  12. 12.
    Halbwachs, N., Proy, Y.-E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. FMSD 11(2) (1997)Google Scholar
  13. 13.
    Healy, C.A., Sjodin, M., Rustagi, V., Whalley, D.B., van Engelen, R.: Supporting timing analysis by automatic bounding of loop iterations. Real-Time Systems 18(2/3), 129–156 (2000)CrossRefGoogle Scholar
  14. 14.
    Lisper, B.: Fully automatic, parametric worst-case execution time analysis. In: WCET (2003)Google Scholar
  15. 15.
    Métayer, D.L.: Ace: An Automatic Complexity Evaluator. ACM Trans. Program. Lang. Syst. 10(2), 248–266 (1988)CrossRefGoogle Scholar
  16. 16.
    Navas, J., Mera, E., López-García, P., Hermenegildo, M.V.: User-definable resource bounds analysis for logic programs. In: Dahl, V., Niemelä, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 348–363. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  17. 17.
    Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32–41. IEEE, Los Alamitos (2004)Google Scholar
  18. 18.
    Rosendahl, M.: Automatic Complexity Analysis. In: FPCA, pp. 144–156 (1989)Google Scholar
  19. 19.
    Wegbreit, B.: Mechanical Program Analysis. Commun. ACM 18(9), 528–539 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D., Bernat, G., Ferdinand, C., Heckmann, R., Mueller, F., Puaut, I., Puschner, P., Staschulat, J., Stenström, P.: The Determination of Worst-Case Execution Times—Overview of the Methods and Survey of Tools. ACM Transactions on Embedded Computing Systems (TECS) (2007)Google Scholar
  21. 21.
    Wilhelm, R., Wachter, B.: Abstract interpretation with applications to timing validation. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 22–36. Springer, Heidelberg (2008)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Sumit Gulwani
    • 1
  1. 1.Microsoft ResearchRedmondUSA

Personalised recommendations