Exact runtime analysis using automata-based symbolic simulation

In this paper, we present a technique for determining tight bounds on the execution time of assembler programs. Thus, our method is independent of the design flow, but takes into account the target architecture to obtain accurate estimates. The key idea is to compute the maximal number of executed instructions by means of symbolic simulation. To this end, we utilize a slight extension of Presburger arithmetic that can be translated to finite automata. Finite automata are an efficient data structure for symbolically traversing the state space of a program.