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

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)