Evaluating the worst-case execution time (WCET) of programs is a very important goal in the design of critical real-time systems. The WCET depends of course of the execution architecture, but also of the semantics of the program. In particular, it is influenced by the feasibility of executions paths in the code. This project aims at applying moderns semantic analysis techniques to detect unfeasible paths, or to bound the number of possible executions of code fragments. In particular, it will consider the expression of properties which are relevant for the WCET, in term of properties that can be analysed by existing tools. These tools may have to be adapted or improved to give the expected results. The student will acquire competences in program static analysis and compilation. The project may be continued by a thesis.
Context: W-SEPT project (ANR)
Contact: Nicolas Halbwachs, Claire Maiza (first.name@imag.fr)
