Compositional solution space quantification for probabilistic software analysis

Abstract

Probabilistic software analysis aims at quantifying how likely a target event is to occur during program execution. Current approaches rely on symbolic execution to identify the conditions to reach the target event and try to quantify the fraction of the input domain satisfying these conditions. Precise quantification is usually limited to linear constraints, while only approximate solutions can be provided in general through statistical approaches. However, statistical approaches may fail to converge to an acceptable accuracy within a reasonable time.

We present a compositional statistical approach for the efficient quantification of solution spaces for arbitrarily complex constraints over bounded floating-point domains. The approach leverages interval constraint propagation to improve the accuracy of the estimation by focusing the sampling on the regions of the input domain containing the sought solutions. Preliminary experiments show significant improvement on previous approaches both in results accuracy and analysis time.

References

1. Mathematica NIntegrate, 2013. http://reference.wolfram.com/mathematica/ref/NIntegrate.html.
2. VolComp, 2013. http://systems.cs.colorado.edu/research/cyberphysical/probabilistic-program-analysis/.
3. A. Adje, O. Bouissou, E. Goubault, J. Goubault-Larrecq, and S. Putot. Static analysis of programs with imprecise probabilistic inputs. In Verified Software: Theories, Tools and Experiments (VSTTE'13), 2013.
4. L. Baresi, E. Di Nitto, and C. Ghezzi. Toward open-world software: Issues and challenges. Computer, 39(10):36--43, 2006.
5. O. Bouissou, E. Goubault, J. Goubault-Larrecq, and S. Putot. A generalization of p-boxes to affine arithmetic. Computing, 94:189--201, 2012.
6. C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler. Exe: Automatically generating inputs of death. ACM Transactions on Information and System Security, 12(2):10:1--10:38, 2008.
7. L. A. Clarke. A system to generate test data and symbolically execute programs. IEEE TSE, 2(3):215--222, 1976.
8. E. Davis. Constraint propagation with interval labels. Artificial Intelligence, 32(3):281--331, July 1987.
9. J. A. De Loera, B. Dutra, M. Köppe, S. Moreinis, G. Pinto, and J. Wu. Software for Exact Integration of Polynomials Over Polyhedra. ACM Communications in Computer Algebra, 45(3/4):169--172, 2012.
10. M. D. Ernst, J. H. Perkins, P. J. Guo, S. McCamant, C. Pacheco, M. S. Tschantz, and C. Xiao. The Daikon System for Dynamic Detection of Likely Invariants. SCP, 69(1--3):35--45, 2007.
11. A. Filieri, C. S. Pasareanu, and W. Visser. Reliability analysis in symbolic pathfinder. In ICSE, pages 622--631, 2013.
12. J. Geldenhuys, M. B. Dwyer, and W. Visser. Probabilistic symbolic execution. In ISSTA, pages 166--176, 2012.
13. P. Godefroid, N. Klarlund, and K. Sen. Dart: directed automated random testing. In PLDI, pages 213--223, 2005.
14. L. Granvilliers and F. Benhamou. Algorithm 852: Realpaver: an interval solver using constraint satisfaction techniques. ACM Transactions on Mathematical Software, 32:138--156, 2006.
15. R. Haggarty. Fundamentals of mathematical analysis. Addison-Wesley New York, 1989.
16. A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker. PRISM: A Tool for Automatic Verification of Probabilistic Systems. In TACAS, pages 441--444. 2006.
17. F. James. Monte carlo theory and practice. Reports on Progress in Physics, 43(9):1145, 1980.
18. J. C. King. Symbolic execution and program testing. Communications of the ACM, 19(7):385--394, July 1976.
19. D. P. Kroese, T. Taimre, and Z. I. Botev. Handbook of Monte Carlo Methods, volume 706. John Wiley & Sons, 2011.
20. M. Kwiatkowska. Quantitative verification: Models, techniques and tools. In ESEC-FSE, pages 449--458, 2007.
21. M. A. Malcolm and R. B. Simpson. Local versus global strategies for adaptive quadrature. ACM Transactions on Mathematical Software, 1 (2):129--146, June 1975.
22. D. Monniaux. An abstract monte-carlo method for the analysis of probabilistic programs. In POPL, pages 93--101, 2001.
23. C. S. Pasareanu, J. Schumann, P. Mehlitz, M. Lowry, G. Karasai, H. Nine, and S. Neema. Model based analysis and test generation for flight software. In SMC-IT, pages 83--90, 2009.
24. C. S. Pasareanu, W. Visser, D. H. Bushnell, J. Geldenhuys, P. C. Mehlitz, and N. Rungta. Symbolic pathfinder: integrating symbolic execution with model checking for java bytecode analysis. Autom. Softw. Eng., 20(3):391--425, 2013.
25. E. Pavese, V. A. Braberman, and S. Uchitel. Automated reliability estimation over partial systematic explorations. In ICSE, pages 602--611, 2013.
26. W. Pestman. Mathematical Statistics. De Gruyter, 2009.
27. W. H. Press, S. A. Teukolsky, W. T. Vetterling, and B. P. Flannery. Numerical Recipes: The Art of Scientific Computing. Cambridge University Press, 3 edition, 2007.
28. C. S. Păsăreanu and N. Rungta. Symbolic pathfinder: symbolic execution of java bytecode. ASE, pages 179--180. ACM, 2010.
29. C. P. Robert and G. Casella. Monte Carlo Statistical Methods. Springer-Verlag New York, Inc., 2005.
30. S. Sankaranarayanan, A. Chakarov, and S. Gulwani. Static analysis for probabilistic programs: inferring whole program properties from finitely many paths. In PLDI, pages 447--458, 2013.
31. N. Tillmann and J. de Halleux. Pex-white box test generation for .net. In TAP, pages 134--153, 2008.
32. P. Zuliani, C. Baier, and E. M. Clarke. Rare-event verification for stochastic hybrid systems. In HSCC, pages 217--226, 2012.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification