Skip to main content


Complete, high-assurance determination of loop bounds and infeasible paths for WCET analysis


Thomas Sewell, Chi Kam and Gernot Heiser




Worst-case execution time (WCET) analysis of real-time code needs to be performed on the executable binary code for soundness. Determination of loop bounds and elimination of infeasible paths, essential for obtaining tight bounds, frequently depends on program state that is difficult to extract from static analysis of the binary. Obtaining this information generally requires manual intervention, or compiler modifications to preserve more semantic information from the source program.

We propose an alternative approach, which leverages an existing translation-validation framework, to enable high-assurance, automatic determination of loop bounds and infeasible path. We show that this approach automatically determines all loop bounds as well as many (possibly all) infeasible paths in the seL4 microkernel, as well as in standard WCET benchmarks which are in the language subset of our C parser.

BibTeX Entry

    author           = {Sewell, Thomas and Kam, Felix and Heiser, Gernot},
    year             = {2016},
    month            = {apr},
    keywords         = {wcet, sel4, real-time, translation validation},
    title            = {Complete, High-Assurance Determination of Loop Bounds and Infeasible Paths for {WCET} Analysis},
    booktitle        = {IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS)},
    address          = {Vienna, Austria}