Loop Bound Analysis based on a Combination of Program Slicing, Abstract Interpretation, and Invariant Analysis

Ermedahl, Andreas; Sandberg, Christer; Gustafsson, Jan; Bygde, Stefan; Lisper, Björn

doi:10.4230/OASIcs.WCET.2007.1194

Document

Loop Bound Analysis based on a Combination of Program Slicing, Abstract Interpretation, and Invariant Analysis

Authors Andreas Ermedahl, Christer Sandberg, Jan Gustafsson, Stefan Bygde, Björn Lisper

Part of: Volume: 7th International Workshop on Worst-Case Execution Time Analysis (WCET'07) (WCET 2007)
Part of: Series: Open Access Series in Informatics (OASIcs)
Part of: Conference: Workshop on Worst-Case Execution Time Analysis (WCET)
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
Publication Date: 2007-11-13

PDF

File

OASIcs.WCET.2007.1194.pdf

Filesize: 166 kB
6 pages

Document Identifiers

DOI: 10.4230/OASIcs.WCET.2007.1194
URN: urn:nbn:de:0030-drops-11946

Author Details

Andreas Ermedahl

Christer Sandberg

Jan Gustafsson

Stefan Bygde

Björn Lisper

Cite AsGet BibTex

Andreas Ermedahl, Christer Sandberg, Jan Gustafsson, Stefan Bygde, and Björn Lisper. Loop Bound Analysis based on a Combination of Program Slicing, Abstract Interpretation, and Invariant Analysis. In 7th International Workshop on Worst-Case Execution Time Analysis (WCET'07). Open Access Series in Informatics (OASIcs), Volume 6, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)
https://doi.org/10.4230/OASIcs.WCET.2007.1194

Abstract

Static Worst-Case Execution Time (WCET) analysis is a technique to derive upper bounds for the execution times of programs. Such bounds are crucial when designing and verifying real-time systems. A key component for static derivation of precise WCET estimates is upper bounds on the number of times different loops can be iterated. In this paper we present an approach for deriving upper loop bounds based on a combination of standard program analysis techniques. The idea is to bound the number of different states in the loop which can influence the exit conditions. Given that the loop terminates, this number provides an upper loop bound. An algorithm based on the approach has been implemented in our WCET analysis tool SWEET. We evaluate the algorithm on a number of standard WCET benchmarks, giving evidence that it is capable to derive valid bounds for many types of loops.

Keywords

WCET analysis
loop-bound analysis
program slicing
abstract interpretation
invariant analysis

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail