[Zurück]

J. Knoop, L. Kovacs, J. Zwirchmayr:
"Practical Experiments with Symbolic Loop Bound Computation for WCET Analysis";
Vortrag: 28. Workshop der GI-Fachgruppe "Programmiersprachen und Rechenkonzepte", Bad Honnef; 02.05.2011 - 04.05.2011; in: "28. Workshop der GI-Fachgruppe Programmiersprachen & Rechenkonzepte", Technischer Bericht des Instituts für Informatik der Christian-Albrechts Universität zu Kiel, (2011).

We present an automatic method for computing tight upper bounds
on the iteration number of special classes of program loops. These upper bounds
are further used in the WCET analysis of programs. Program flow is refined us-
ing SMT reasoning, rewriting multi-path loops into single-path ones. Single-path
loops are further translated into a set of recurrence relations over program vari-
ables. To solve recurrences, we deploy pattern-based technique, instantiating pre-
computed closed forms for a restricted class of recurrence equations. In practice,
these recurrences describe the behavior of a large set of program loops relevant
in the WCET community. Our technique is implemented in the r-TuBound tool
and was successfully tried out on a number of WCET benchmarks.

smacc, sw verification, SMT, SAT, symbolic execution, symbolic simulation

http://publik.tuwien.ac.at/files/PubDat_198263.pdf