February 4, 2013

Vitor Rodrigues (Université d'Orléans) salle des thèses

Modern real-time systems demand safe determination of bounds on the execution times of programs. To this purpose, program execution for all possible combinations of input values is impracticable. In alternative, static analysis methods provide sound and efficient mechanisms for determining execution time bounds, regardless of knowledge on input data. We present a calculational and compositional development of a functional static analyzer using the theory of abstract interpretation. A particular instantiation of our data flow framework was created for the static analysis of the “worst-case execution time” (WCET) of a program running on multicore systems. The entire system is implemented in Haskell, with the objective to take advantages of the declarative features of the language for a simpler and more robust specification of the underlying concepts.