AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
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

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

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

Cited by: 113|Views161
EI

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:

0
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]
Tables
  • 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
Download tables as Excel
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.
    Google ScholarLocate open access versionFindings
  • S. Arora and B. Barak. Computational Complexity: A Modern Approach. Cambridge University Press, 2009.
    Google ScholarFindings
  • O. Bouissou, E. Goubault, J. Goubault-Larrecq, and S. Putot. A generalization of p-boxes to affine arithmetic. Computing, 2012.
    Google ScholarLocate open access versionFindings
  • S. Chaudhuri and A. Solar-Lezama. Smoothing a program soundly and robustly. In CAV, volume 6806 of LNCS, pages 277–292.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • P. Cousot and M. Monerau. Probabilistic abstract interpretation. In ESOP, volume 7211 of LNCS, pages 169–193.
    Google ScholarLocate open access versionFindings
  • 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.
    Findings
  • 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.
    Google ScholarFindings
  • A. Dempster. A generalization of bayesian inference. Journal of the Royal Statistical Society, 30:205–247, 1968.
    Google ScholarLocate open access versionFindings
  • [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).
    Google ScholarLocate open access versionFindings
  • [12] D. Frenkel and B. Smit. Understanding Molecular Simulation: From Algorithms to Applications. Academic Press, 2002.
    Google ScholarFindings
  • [13] J. Geldenhuys, M. B. Dwyer, and W. Visser. Probabilistic symbolic execution. In ISSTA, pages 166–176. ACM, 2012.
    Google ScholarLocate open access versionFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • [16] H. Hermanns, B. Wachter, and L. Zhang. Probabilistic CEGAR. In CAV, volume 5123 of LNCS, pages 162–175.
    Google ScholarLocate open access versionFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • [18] R. Jhala and R. Majumdar. Path slicing. In PLDI ’05, pages 38–47. ACM, 2005.
    Google ScholarLocate open access versionFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • [21] D. Kozen. Semantics of probabilistic programs. J. Computer and System Sciences, 22:328–350, 1981.
    Google ScholarLocate open access versionFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • [24] Kwiatkowska et al. The PRISM model checker. http://www.prismmodelchecker.org.
    Findings
  • [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.
    Google ScholarLocate open access versionFindings
  • [26] A. McIver and C. Morgan. Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, 2004.
    Google ScholarFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • [28] D. Monniaux. An abstract monte-carlo method for the analysis of probabilistic programs. In POPL, pages 93–101. ACM, 2001.
    Google ScholarLocate open access versionFindings
  • [29] D. Monniaux. Abstract interpretation of programs as markov decision processes. Sci. Comput. Program., 58(1-2):179–205, 2005.
    Google ScholarLocate open access versionFindings
  • [30] R. Motwani and P. Raghavan. Randomized Algorithms. Cambridge University Press, 1995.
    Google ScholarFindings
  • [31] A. Pfeffer. IBAL: a probabilistic rational programming language. In In Proc. 17th IJCAI, pages 733–740. Morgan Kaufmann Publishers, 2001.
    Google ScholarLocate open access versionFindings
  • [32] A. D. Pierro, C. Hankin, and H. Wiklicky. Probabilistic λ-calculus and quantitative program analysis. J. Logic and Computation, 15(2): 159–179, 2005.
    Google ScholarLocate open access versionFindings
  • [33] A. Radul. Report on the probabilistic language scheme. In DLS, pages 2–10. ACM, 2007.
    Google ScholarLocate open access versionFindings
  • [34] R. Y. Rubinstein and D. P. Kroese. Simulation and the Monte Carlo Method. Wiley Series in Probability and Mathematical Statistics, 2008.
    Google ScholarLocate open access versionFindings
  • [35] G. Shafer. A Mathematical Theory of Evidence. Princeton University Press, 1976.
    Google ScholarFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • [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.
    Google ScholarLocate open access versionFindings
Your rating :
0

 

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