[Back]

B. Rieder, P. Puschner, I. Wenzel:
"Using Model Checking to Derive Loop Bounds of General Loops within ANSI-C Applications for Measurement Based WCET Analysis";
Talk: Workshop on Intelligent Solutions in Embedded Systems (WISES'08), Regensburg, Germany; 2008-07-10 - 2008-07-11; in: "Proceedings of the Sixth Workshop on Intelligent Solutions in Embedded Systems", IEEE Computer Society, (2008), ISBN: 978-3-00-024989-1; 3 - 9.

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.