Title
Symbolic loop bound computation for WCET analysis
Abstract
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. To do so, we refine program flows using SMT reasoning and rewrite multi-path loops into single-path ones. Single-path loops are further translated into a set of recurrence relations over program variables. Recurrence relations are solved and iteration bounds of program loops are derived from the computed closed forms. For solving recurrences we deploy a pattern-based recurrence solving algorithm and compute closed forms only for a restricted class of recurrence equations. However, in practice, these recurrences describe the behavior of a large set of program loops. Our technique is implemented in the r-TuBound tool and was successfully tried out on a number of challenging WCET benchmarks.
Year
DOI
Venue
2011
10.1007/978-3-642-29709-0_20
Ershov Memorial Conference
Keywords
Field
DocType
wcet analysis,iteration bound,program variable,wcet benchmarks,pattern-based recurrence,computed closed form,program loop,symbolic loop,iteration number,recurrence relation,recurrence equation
Algebra,Abstract interpretation,Recurrence relation,Computer science,Recurrence equations,Theoretical computer science,Computation
Conference
Citations 
PageRank 
References 
10
0.59
18
Authors
3
Name
Order
Citations
PageRank
Jens Knoop183874.76
Laura Kovács249436.97
Jakob Zwirchmayr3544.19