20
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Bounded Expectations: Resource Analysis for Probabilistic Programs

      Preprint
      , ,

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          This paper presents a new static analysis for deriving upper bounds on the expected resource consumption of probabilistic programs. The analysis is fully automatic and derives symbolic bounds that are multivariate polynomials of the inputs. The new technique combines manual state-of-the-art reasoning techniques for probabilistic programs with an effective method for automatic resource-bound analysis of deterministic programs. It can be seen as both, an extension of automatic amortized resource analysis (AARA) to probabilistic programs and an automation of manual reasoning for probabilistic programs that is based on weakest preconditions. As a result, bound inference can be reduced to off-the-shelf LP solving in many cases and automatically-derived bounds can be interactively extended with standard program logics if the automation fails. Building on existing work, the soundness of the analysis is proved with respect to an operational semantics that is based on Markov decision processes. The effectiveness of the technique is demonstrated with a prototype implementation that is used to automatically analyze 39 challenging probabilistic programs and randomized algorithms. Experimental results indicate that the derived constant factors in the bounds are very precise and even optimal for many programs.

          Related collections

          Most cited references35

          • Record: found
          • Abstract: not found
          • Conference Proceedings: not found

          Probabilistic programming

            Bookmark
            • Record: found
            • Abstract: not found
            • Book Chapter: not found

            Apron: A Library of Numerical Abstract Domains for Static Analysis

              Bookmark
              • Record: found
              • Abstract: not found
              • Book Chapter: not found

              Probabilistic Program Analysis with Martingales

                Bookmark

                Author and article information

                Journal
                23 November 2017
                Article
                1711.08847
                105a9fea-19ff-4f7d-936e-f5355c58718a

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                History
                Custom metadata
                cs.PL

                Comments

                Comment on this article