Probabilistic Resource Analysis by Program Transformation

TL;DR

This paper introduces an automated method for probabilistic resource analysis of C programs, transforming complex resource usage distributions into closed-form expressions through program rewriting and over-approximations.

Contribution

It presents a novel multi-phase rewriting approach for deriving resource usage distributions from probabilistic inputs in C programs.

Findings

Successfully analyzed example programs with the system

Generated resource usage distributions in closed form

Demonstrated the effectiveness of the approach

Abstract

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.