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.