Determining concrete bounds for loops is one of the more vexing problems
of resource analysis of realtime programs.  Current mechanisms are
limited in scope and require considerable user input that can not be
verified.  The authors present a methodology for providing more general
loop bounds where the correctness can be demonstrated with formal
techniques.  The methodology combines data flow analysis and deductive
formal verification to attain this goal.