Using model checking to derive loop bounds of general loops within ANSI-C applications for measurement based WCET analysis

Knowing the boundaries of loops is an important prerequisite for both, static and dynamic worst case execution time (WCET) analysis. However, loop bound calculation is a complex task of its own, and often more effort than planned has to be put into it. This paper describes a simple and quick method for loop bound calculation using a model checker that cannot only find loop bounds for integer iterator variables but works with practically all kind of loops.