2012-01-28 Verification day

Thao Dang

Reachability analysis for polynomial dynamical systems using the Bernstein expansion

This paper is concerned with the reachability computation problem for polynomial discrete-time dynamical systems. Such computations constitute a crucial component in algorithmic verification tools for hybrid systems and embedded software with polynomial dynamics, which have found applications in many engineering domains. We describe two methods for over-approximating the reachable sets of such systems; these methods are based on a combination of the Bernstein expansion of polynomial functions and a representation of reachable sets by template polyhedra. Using a prototype implementation, the performance of the methods was demonstrated on a number of examples of control systems and biological systems.

• Les besoins pour l'analyse de vulnérabilités

  (Marie-Laure, ~ 20 minutes)
 Nous présentons nos travaux en cours dans le cadre de l'analyse de code vulnérable,
 en insistant notamment sur :
   - les particularités de ce type d'analyse : code binaire, modèle mémoire ad hoc
   - les conséquences sur les techniques d'analyse à utiliser ou développer

• Analyse de teinte sur du code binaire

 (Laurent, ~ 20 minutes)
 Nous présentons un exemple concret d'analyse développée pour la recherche de
 vulnérabilités : l'analyse de teinte.