Bibtex de la publication

@InProceedings{ deBoCaSa2008.1,
author = {de Michiel, Marianne and Bonenfant, Armelle and Cassé, Hugues and Sainrat, Pascal},
title = "{Static loop bound analysis of C programs based on flow analysis and abstract interpretation}",
booktitle = "{IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA), Kaohsiung, Taiwan, 25/08/2008-27/08/2008}",
year = {2008},
month = {août},
publisher = {IEEE Computer Society},
address = {},
pages = {161--168},
language = {anglais},
URL = {,%20},
keywords = {Static Analysis, Loop bounds, Abstract interpretation,},
abstract = {One of the important steps in processing the worst case execution time (WCET) of a program is to determine the loops upper bounds. Such bounds are crucial when verifying real-time systems. In this paper, we propose a static loop bound analysis which associates flow analysis and abstract interpretation. It considers binary operators (+, -, *, \) for the loop increment, nested loops, non-recursive function calls, simple loop conditions (==, !=,<, <=, >, >=, &&) and loop upper bound values (instead of intervals). We present the result of our analysis on the Mälardalen benchmark suite and compare them to the recent work of Ermedahl et al.}