Replacing conjectures by positive knowledge: Inferring proven precise worst-case execution time bounds using symbolic execution

We implemented our approach in the r-TuBound WCET toolchain and tested it on challenging benchmarks from the WCET community. Our experimental results underline the advantage of using symbolic methods for proving WCET bounds precise, at a moderate cost.