Skip to Main content Skip to Navigation
New interface
Conference papers

Formal Verification of Loop Bound Estimation for WCET Analysis

Sandrine Blazy 1 André Maroneze 1 David Pichardie 1 
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Worst-case execution time (WCET) estimation tools are complex pieces of software performing tasks such as computation on control flow graphs (CFGs) and bound calculation. In this paper, we present a formal verification (in Coq) of a loop bound estimation. It relies on program slicing and bound calculation. The work has been integrated into the CompCert verified C compiler. Our verified analyses directly operate on non-structured CFGs. We extend the CompCert RTL intermediate language with a notion of loop nesting (a.k.a. weak topological ordering on CFGs) that is useful for reasoning on CFGs. The automatic extraction of our loop bound estimation into OCaml yields a program with competitive results, obtained from experiments on a reference benchmark for WCET bound estimation tools.
Document type :
Conference papers
Complete list of metadata

Cited literature [24 references]  Display  Hide  Download
Contributor : Sandrine Blazy Connect in order to contact the contributor
Submitted on : Sunday, July 28, 2013 - 8:10:56 AM
Last modification on : Wednesday, February 2, 2022 - 3:50:51 PM
Long-term archiving on: : Wednesday, April 5, 2017 - 5:17:04 PM


Files produced by the author(s)


  • HAL Id : hal-00848703, version 1


Sandrine Blazy, André Maroneze, David Pichardie. Formal Verification of Loop Bound Estimation for WCET Analysis. VSTTE - Verified Software: Theories, Tools and Experiments, Natarajan Shankar, May 2013, Menlo Park, United States. pp.281-303. ⟨hal-00848703⟩



Record views


Files downloads