2012-01-28 Verification day

From STATOR
Revision as of 14:04, 17 January 2013 by David Monniaux (talk | contribs)
Jump to navigation Jump to search

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.