R-tubound: Loop bounds for WCET analysis. We describe the structure and the usage of a new software tool, called r-TuBound, for deriving symbolic loop iteration bounds in the worst-case execution time (WCET) analysis of programs. r-TuBound implements algorithms for pattern-based recurrence solving and program flow refinement, and it was successfully tested on a wide range of examples. The purpose of this article is to illustrate what r-TuBound can do and how it can be used to derive the WCET of programs.
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Knoop, Jens; Kovács, Laura; Zwirchmayr, Jakob: Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution (2017)
- Biere, Armin; Knoop, Jens; Kovács, Laura; Zwirchmayr, Jakob: Smacc: a retargetable symbolic execution engine (2013) ioport
- Knoop, Jens; Kovács, Laura; Zwirchmayr, Jakob: R-tubound: Loop bounds for WCET analysis (Tool paper) (2012) ioport