## AI helps you reading Science

## AI Insight

AI extracts a summary of this paper

Weibo:

# Static analysis for probabilistic programs: inferring whole program properties from finitely many paths

PLDI, no. 6 (2013): 447-458

EI

Keywords

Abstract

We propose an approach for the static analysis of probabilistic programs that sense, manipulate, and control based on uncertain data. Examples include programs used in risk analysis, medical decision making and cyber-physical systems. Correctness properties of such programs take the form of queries that seek the probabilities of assertion...More

Code:

Data:

Introduction

- The goal of this paper is to study static analysis techniques for proving properties of probabilistic programs that manipulate uncertain quantities defined by probability distributions.
- The authors present an approach to infer bounds on assertion probability for the whole program by considering a suitably chosen finite set of program paths.
- The computation of path probabilities reduces to the problem of estimating the probability that a sample point from R drawn according to the distribution of the individual variables satisfies φ.

Highlights

- The goal of this paper is to study static analysis techniques for proving properties of probabilistic programs that manipulate uncertain quantities defined by probability distributions
- Uncertainty is a common aspect of many software systems, especially systems that manipulate error-prone data to make medical decisions; systems that predict long term risks of catastrophic events such as floods and earthquakes; and control systems that operate in the presence of sensor errors and external environmental disturbances
- Symbolic execution is performed along the collected paths, yielding the path conditions and transforming the probabilistic queries into assertions involving the random variables produced along the path
- Any viable solution for infinite state probabilistic programs must restrict the set of programs analyzed through some syntactic or semantic criteria, or deal with information loss due to the abstraction of intermediate probability distributions
- We have developed an analysis framework for probabilistic programs based on considering finitely many paths and estimating the probability of the remainder

Results

- The authors address the issue of computing bounds on the probability of a given polyhedral set specified by assertion φ over a set of real-valued variables Q = {r1, .
- Symbolic execution is performed along the collected paths, yielding the path conditions and transforming the probabilistic queries into assertions involving the random variables produced along the path.
- The probability bounds computation performs well on many of the examples, solving large problems with as many as 50 integer and real variables.
- The execution of small and seemingly simple programs that use standard uniform random number generators can yield complex probability distributions over the program variables.
- Analysis algorithms for probabilistic programs must provide solutions to three basic questions: (a) Representing the possible intermediate distributions of variables, (b) Propagating the chosen representation according to the program semantics, and (c) Reasoning about the probabilities of assertions using the given intermediate distribution representation.
- The sources of loss in the approach include the probability bounds computation and the unexplored program paths.
- Whereas the techniques described so far perform a forward propagation of the distribution information, it is possible to use backward abstract interpretation starting from an assertion whose probability is to be established, and exploring its preconditions backwards along the program paths.
- A key problem lies in relating the results of the analysis proposed by DiPierro et al that provide a “close approximation” to the probability of a query assertion with the “classical” approach that provides a guaranteed interval bound enclosing the actual probability, such as the approach presented in this paper.

Conclusion

- Geldenhuys et al proposed the integration of symbolic execution with exact model counting techniques to estimate the probabilities of violating assertions along individual paths of the program [13].
- The authors observed two limitations of LattE that make it less ideal for probabilistic program analysis tasks: (a) the existing implementation does not handle non-uniform distributions, and (b) exact volume determination for real polyhedra is quite expensive, and often runs out of time/memory on the constraints that are obtained from the benchmarks.
- The authors' future work will focus on more efficient polyhedral probability estimators using ellipsoidal and zonotope approximations, and the problem of synthesizing sketches, complementing recent approaches to this problem [4]

- Table1: Queries on the final state of the program and their informal meaning
- Table2: Specification of the inbuilt random value generators. Note that the function 1⁄2X (x) is the indicator function for the set X
- Table3: Primitives needed for each distribution type to support probability and expectation estimation
- Table4: Benchmarks used in our evaluation with descriptions. The benchmarks are available on-line at our project page, or upon request. #var: number of input variables to the program. + indicates random value generation inside loops
- Table5: Experimental evaluation of initial adequate path exploration strategy. Our coverage goal was c = 0.95 at a 95% confidence level. Ns, Nu: number of simulated paths and unique paths, respectively, Ts: simulation time in seconds, Tvc: total volume computation time (branch-and-bound depth is set to 15), pmc: monte-carlo probability estimate, [lb, ub]: coverage bounds
- Table6: Query processing results on the benchmark examples

Funding

- Sankaranarayanan and Chakarov acknowledge support from the US National Science Foundation (NSF) under award numbers CNS-0953941, CNS-1016994 and CPS-1035845

Reference

- C. C. Aggarwal and P. S. Yu. A survey of uncertain data algorithms and applications. IEEE Transactions on Knowledge and Data Engineering (TKDE), 21(5), May 2009.
- S. Arora and B. Barak. Computational Complexity: A Modern Approach. Cambridge University Press, 2009.
- O. Bouissou, E. Goubault, J. Goubault-Larrecq, and S. Putot. A generalization of p-boxes to affine arithmetic. Computing, 2012.
- S. Chaudhuri and A. Solar-Lezama. Smoothing a program soundly and robustly. In CAV, volume 6806 of LNCS, pages 277–292.
- E. Clarke, A. Donze, and A. Legay. Statistical model checking of analog mixed-signal circuits with an application to a third order δ − σ modulator. In Hardware and Software: Verification and Testing, volume 5394/2009 of LNCS, pages 149–163, 2009.
- P. Cousot and M. Monerau. Probabilistic abstract interpretation. In ESOP, volume 7211 of LNCS, pages 169–193.
- L. H. de Figueiredo and J. Stolfi. Self-validated numerical methods and applications. In Brazilian Mathematics Colloquium monograph. IMPA, Rio de Janeiro, Brazil, 199Cf. http://www.ic.unicamp.br/~stolfi/EXPORT/papers/by-tag/fig-sto-97-iaaa.ps.gz.
- J. De Loera, B. Dutra, M. Koeppe, S. Moreinis, G. Pinto, and J. Wu. Software for Exact Integration of Polynomials over Polyhedra. ArXiv e-prints, July 2011.
- A. Dempster. A generalization of bayesian inference. Journal of the Royal Statistical Society, 30:205–247, 1968.
- [11] A. Filieri, C. S. Pasareanu, and W. Visser. Reliability analysis in symbolic pathfinder. In Intl. Conference on Software Engg. (ICSE), 2013. (To Appear, May 2013).
- [12] D. Frenkel and B. Smit. Understanding Molecular Simulation: From Algorithms to Applications. Academic Press, 2002.
- [13] J. Geldenhuys, M. B. Dwyer, and W. Visser. Probabilistic symbolic execution. In ISSTA, pages 166–176. ACM, 2012.
- [14] N. D. Goodman, V. K. Mansinghka, D. M. Roy, K. Bonawitz, and J. B. Tenenbaum. Church: a language for generative models. In Uncertainty in Artificial Intelligence, pages 220–229, 2008.
- [15] L. Granvilliers and F. Benhamou. Algorithm 852: Realpaver: an interval solver using constraint satisfaction techniques. ACM Trans. On Mathematical Software, 32(1):138–156, 2006.
- [16] H. Hermanns, B. Wachter, and L. Zhang. Probabilistic CEGAR. In CAV, volume 5123 of LNCS, pages 162–175.
- [17] S. K. Jha, E. M. Clarke, C. J. Langmead, A. Legay, A. Platzer, and P. Zuliani. A bayesian approach to model checking biological systems. In CMSB, volume 5688 of Lecture Notes in Computer Science, pages 218–234.
- [18] R. Jhala and R. Majumdar. Path slicing. In PLDI ’05, pages 38–47. ACM, 2005.
- [19] C. Jones, G. McQuillan, and et al. Serum creatinine levels in the US population: Third national health and nutrition examination survey. Am. J. Kidney Disease, 32(6):992–999, 1998.
- [20] J.-P. Katoen, A. McIver, L. Meinicke, and C. Morgan. Linear-invariant generation for probabilistic programs. In Static Analysis Symposium (SAS), volume 6337 of LNCS, page 390406. Springer, 2010.
- [21] D. Kozen. Semantics of probabilistic programs. J. Computer and System Sciences, 22:328–350, 1981.
- [22] M. Kwiatkowska, G. Norman, and D. Parker. A framework for verification of software with time and probabilities. In FORMATS, volume 6246 of LNCS, pages 25–45.
- [23] M. Kwiatkowska, G. Norman, and D. Parker. PRISM 4.0: Verification of probabilistic real-time systems. In CAV, volume 6806 of LNCS, pages 585–591.
- [24] Kwiatkowska et al. The PRISM model checker. http://www.prismmodelchecker.org.
- [25] P. Mardziel, S. Magill, M. Hicks, and M. Srivatsa. Dynamic enforcement of knowledge-based security policies. In Computer Security Foundations Symposium (CSF), pages 114–128, JUN 2011.
- [26] A. McIver and C. Morgan. Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, 2004.
- [27] S. Misailovic, D. M. Roy, and M. C. Rinard. Probabilistically accurate program transformations. In Static Analysis Symposium, volume 6887 of LNCS, pages 316–333.
- [28] D. Monniaux. An abstract monte-carlo method for the analysis of probabilistic programs. In POPL, pages 93–101. ACM, 2001.
- [29] D. Monniaux. Abstract interpretation of programs as markov decision processes. Sci. Comput. Program., 58(1-2):179–205, 2005.
- [30] R. Motwani and P. Raghavan. Randomized Algorithms. Cambridge University Press, 1995.
- [31] A. Pfeffer. IBAL: a probabilistic rational programming language. In In Proc. 17th IJCAI, pages 733–740. Morgan Kaufmann Publishers, 2001.
- [32] A. D. Pierro, C. Hankin, and H. Wiklicky. Probabilistic λ-calculus and quantitative program analysis. J. Logic and Computation, 15(2): 159–179, 2005.
- [33] A. Radul. Report on the probabilistic language scheme. In DLS, pages 2–10. ACM, 2007.
- [34] R. Y. Rubinstein and D. P. Kroese. Simulation and the Monte Carlo Method. Wiley Series in Probability and Mathematical Statistics, 2008.
- [35] G. Shafer. A Mathematical Theory of Evidence. Princeton University Press, 1976.
- [36] W. Visser, J. Geldenhuys, and M. B. Dwyer. Green: reducing, reusing and recycling constraints in program analysis. In SIGSOFT FSE, page 58. ACM, 2012.
- [37] H. L. S. Younes and R. G. Simmons. Statistical probabilitistic model checking with a focus on time-bounded properties. Information & Computation, 204(9):1368–1409, 2006.

Tags

Comments

数据免责声明

页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果，我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问，可以通过电子邮件方式联系我们：report@aminer.cn