Probabilistic Resource Analysis by Program Transformation

  • Maja H. KirkebyEmail author
  • Mads Rosendahl
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9964)


The aim of a probabilistic resource analysis is to derive a probability distribution of possible resource usage for a program from a probability distribution of its input. We present an automated multi-phase rewriting based method to analyze programs written in a subset of C. It generates a probability distribution of the resource usage as a possibly uncomputable expression and then transforms it into a closed form expression using over-approximations. We present the technique, outline the implementation and show results from experiments with the system.


Resource Usage Probabilistic Semantic Argument Development Recursive Program Intermediate Language 
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.
    Adje, A., Bouissou, O., Goubault-Larrecq, J., Goubault, E., Putot, S.: Static analysis of programs with imprecise probabilistic inputs. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 22–47. Springer, Heidelberg (2014). doi: 10.1007/978-3-642-54108-7_2 CrossRefGoogle Scholar
  2. 2.
    Bauer, M.: Approximations for decision making in the Dempster-Shafer theory of evidence. In: Horvitz, E., Jensen, F.V. (eds.) UAI, pp. 73–80. Morgan Kaufmann (1996)Google Scholar
  3. 3.
    Berleant, D., Cheng, H.: A software tool for automatically verified operations on intervals and probability distributions. Reliable Comput. 4(1), 71–82 (1998)CrossRefzbMATHGoogle Scholar
  4. 4.
    Bouissou, O., Goubault, E., Goubault-Larrecq, J., Putot, S.: A generalization of p-boxes to affine arithmetic. Computing 94(2–4), 189–201 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Bueno, F., Cabeza, D., Carro, M., Hermenegildo, M., López-Garcıa, P., Puebla, G.: The ciao prolog system. Reference Manual. The Ciao System Documentation Series-TR CLIP3/97.1, School of Computer Science, Technical University of Madrid (UPM), vol. 95, p. 96 (1997)Google Scholar
  6. 6.
    Cousot, P., Monerau, M.: Probabilistic abstract interpretation. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 169–193. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-28869-2_9 CrossRefGoogle Scholar
  7. 7.
    Debray, S.K., García, P.L., Hermenegildo, M., Lin, N.-W.: Estimating the computational cost of logic programs. In: Charlier, B. (ed.) SAS 1994. LNCS, vol. 864, pp. 255–265. Springer, Heidelberg (1994). doi: 10.1007/3-540-58485-4_45 CrossRefGoogle Scholar
  8. 8.
    Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19(5), 236–243 (1976)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Destercke, S., Dubois, D.: The role of generalised p-boxes in imprecise probability models. In: 6th International Symposium on Imprecise Probability: Theories and Applications (2009)Google Scholar
  10. 10.
    Ferson, S.: Model uncertainty in risk analysis. Technical report, Centre de Recherches de Royallieu, Universite de Technologie de Compiegne (2014)Google Scholar
  11. 11.
    Ferson, S., Kreinovich, V., Ginzburg, L., Myers, D.S., Sentz, K.: Constructing probability boxes and Dempster-Shafer structures. Sand 2002–4015, Sandia National Laboratories (2002)Google Scholar
  12. 12.
    Flajolet, P., Salvy, B., Zimmermann, P.: Automatic average-case analysis of algorithm. Theor. Comput. Sci. 79(1), 37–109 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53–113. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-21455-4_3 CrossRefGoogle Scholar
  14. 14.
    Gao, A.: Modular average case analysis: Language implementation and extension. Ph.d. thesis, University College Cork (2013)Google Scholar
  15. 15.
    Geldenhuys, J., Dwyer, M.B., Visser, W.: Probabilistic symbolic execution. In: Proceedings of the 2012 International Symposium on Software Testing and Analysis, pp. 166–176. ACM (2012)Google Scholar
  16. 16.
    Gordon, J., Shortliffe, E.H.: The Dempster-Shafer theory of evidence. In: Rule-Based Expert Systems: The MYCIN Experiments of the Stanford Heuristic Programming Project, p. 21 (1984)Google Scholar
  17. 17.
    Guo, X., Boubekeur, M., McEnery, J., Hickey, D.: ACET based scheduling of soft real-time systems: an approach to optimise resource budgeting. Int. J. Comput. Commun. 1(1), 82–86 (2007)Google Scholar
  18. 18.
    Kay, R.U.: Fundamentals of the Dempster-Shafer theory and its applications to system safety and reliability modelling. In: RTA, pp. 173–185 (2007)Google Scholar
  19. 19.
    Kerrison, S., Eder, K.: Energy modelling and optimisation of software for a hardware multi-threaded embedded microprocessor. University of Bristol, Bristol, Technical report (2013)Google Scholar
  20. 20.
    Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328–350 (1981)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Kwiatkowska, M., Norman, G., Parker, D.: Advances and challenges of probabilistic model checking. In: 48th Annual Allerton Conference on Communication, Control, and Computing, pp. 1691–1698. IEEE, September 2010Google Scholar
  22. 22.
    Liqat, U., Kerrison, S., Serrano, A., Georgiou, K., Lopez-Garcia, P., Grech, N., Hermenegildo, M.V., Eder, K.: Energy consumption analysis of programs based on XMOS ISA level models. In: Gupta, G., Peña, R. (eds.) LOPSTR 2013. LNCS, vol. 8901, pp. 72–90. Springer, Heidelberg (2013). doi: 10.1007/978-3-319-14125-1_5 Google Scholar
  23. 23.
    Monniaux, D.: Abstract interpretation of probabilistic semantics. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 322–339. Springer, Heidelberg (2000). doi: 10.1007/978-3-540-45099-3_17 CrossRefGoogle Scholar
  24. 24.
    Pierro, A., Hankin, C., Wiklicky, H.: Abstract interpretation for worst and average case analysis. In: Reps, T., Sagiv, M., Bauer, J. (eds.) Program Analysis and Compilation, Theory and Practice. LNCS, vol. 4444, pp. 160–174. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-71322-7_8 CrossRefGoogle Scholar
  25. 25.
    Di Pierro, A., Wiklicky, H., Puppis, G., Villa, T.: Probabilistic data flow analysis: a linear equational approach. In: Proceedings Fourth International Symposium, vol. 119, pp. 150–165. Open Publishing Association (2013)Google Scholar
  26. 26.
    Soza Pollman, H., Carro, M., Lopez Garcia, P.: Probabilistic cost analysis of logic programs: a first case study. INGENIARE - Revista Chilena de Ingeniera 17(2), 195–204 (2009)Google Scholar
  27. 27.
    Rosendahl, M.: Automatic program analysis. Master’s thesis, University of Copenhagen (1986)Google Scholar
  28. 28.
    Rosendahl, M.: Automatic complexity analysis. In: FPCA, pp. 144–156 (1989)Google Scholar
  29. 29.
    Rosendahl, M., Kirkeby, M.H.: Probabilistic output analysis by program manipulation. In: Quantitative Aspects of Programming Languages, EPTCS (2015)Google Scholar
  30. 30.
    Sankaranarayanan, S., Chakarov, A., Gulwani, S.: Static analysis for probabilistic programs: inferring whole program properties from finitely many paths. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 447–458. ACM, June 2013Google Scholar
  31. 31.
    Schellekens, M.P.: A Modular Calculus for the Average Cost of Data Structuring. Springer, New York (2008)CrossRefGoogle Scholar
  32. 32.
    Tiwari, V., Malik, S., Wolfe, A.: Power analysis of embedded software a first step towards software power minimization. IEEE Trans. Very Large Scale Integr. (VLSI) Syst. 2(4), 437–445 (1994)CrossRefGoogle Scholar
  33. 33.
    Uwimbabazi, A.: Extended probabilistic symbolic execution. Master’s thesis, University of Stellenbosch (2013)Google Scholar
  34. 34.
    Volpano, D.M., Irvine, C.E., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2/3), 167–188 (1996)CrossRefGoogle Scholar
  35. 35.
    Wegbreit, B.: Mechanical program analysis. Commun. ACM 18(9), 528–539 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  36. 36.
    Weiser, M.: Program slicing. In: Proceedings of the 5th International Conference on Software Engineering, pp. 439–449. IEEE Press (1981)Google Scholar
  37. 37.
    Wierman, A., Andrew, L.L.H., Tang, A.: Stochastic analysis of power-aware scheduling. In: Proceedings of Allerton Conference on Communication, Control and Computing. Urbana-Champaign, IL (2008)Google Scholar
  38. 38.
    Wilson, N.: Algorithms for Dempster-Shafer theory. In: Kohlas, J., Moral, S. (eds.) Handbook of Defeasible Reasoning and Uncertainty Management Systems. Handbook of Defeasible Reasoning and Uncertainty Management Systems, vol. 5, pp. 421–475. Springer, Netherlands (2000)CrossRefGoogle Scholar
  39. 39.
    Wolfram, S.: The Mathematica Book. Cambridge University Press and Wolfram Research Inc., New York (2000)zbMATHGoogle Scholar
  40. 40.
    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). doi: 10.1007/978-3-642-23702-7_22 CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Computer ScienceRoskilde UniversityRoskildeDenmark

Personalised recommendations