Séminaire ROSP le 2 avril à 14h30 - David Monniaux

Le prochain séminaire ROSP se déroulera le jeudi 2 avril à 14h30 en salle C219 (noté la salle inhabituelle) avec un exposé de David Monniaux (VERIMAG) ayant pour titre : "Worst-case execution time as a combinatorial optimization problem" (résumé en fin de mail).



Worst-case execution time as a combinatorial optimization problem



Bounds on the worst-case execution time of reactive control software, taking into account cache and pipeline effects, can be improved by taking into account infeasible paths. We express the problem as maximization within the solution set of a satisfiability modulo theory (SMT) problem. Unfortunately this generates formulas of a hard class for all solvers based on the DPLL(T) scheme (all production-grade solvers). We thus introduced cuts that make tractable previously intractable problems.

(papier avec Julien Henry et Claire Maiza et Mihail Asavoae publié à LCTES 2014)