The functioning and development of living organisms is controlled on the molecular level by genetic regulatory networks. The switch-like character of genetic regulations has motivated the development of hybrid models of genetic networks. These models describe the dynamics of the networks as a combination of continuous evolutions and discrete events.

In this talk, I will present two classes of hybrid systems that are particularly well adapted to modeling genetic networks, based on piecewise affine or piecewise multiaffine differential equations. Methods have been recently developed for the formal verification of the dynamical properties of these systems. They rely on the use of discrete abstraction and model checking, and have been designed to cope with large uncertainties on the values of the parameters that one often encounters when analyzing these systems. 

These techniques make it possible to assess the validity of a model, by checking the consistency between predictions and experimental data, or to design networks whose behaviors satisfy given temporal specifications.

Work done in collaboration with:\\
Hidde de Jong (INRIA), Johannes Geiselmann (UJF, Grenoble), Jean-Luc Gouz\'e (INRIA), Radu Mateescu (INRIA), Michel Page (UPMF,  Grenoble), Delphine Ropers (INRIA), Tewfik Sari (UHA, Mulhouse), Dominique Schneider (UJF, Grenoble),\\
and with:\\
Calin Belta (Boston Univ.), Boyan Yordanov (Boston Univ.), Ron Weiss (Princeton Univ.).