Automatic flow analysis using symbolic execution and path enumeration

In this paper, we propose a static worst-case execution time (WCET) analysis approach aimed to automatically extract flow information related to program semantics. This information is used to reduce the over estimation of the calculated WCET. We focus on flow information related to loop bounds and infeasible paths. Indeed, this information is at the origin of important overestimation of the WCET. The approach handles loops with multiple exit conditions and non-rectangular loops in which the number of iterations of an inner loop depends on the current iteration of an outer loop. The number of loop iterations is expressed as summations function of the loop bounds. The flow analysis approach combines symbolic execution and path enumeration in order to avoid unfolding loops performed by symbolic execution-based approaches while providing tight and safe WCET estimate