année : 2010
Les travaux récents de Bernot, Comet, et Richard ont démontré tout l'intérêt des méthodes formelles pour la compréhension de la biologie des systèmes. Nous proposons de pousser les investigations plus loin en intégrant la démonstration sur ordinateur, à l'aide d'applications comme Coq, dans la palette d'outils à la disposition du chercheur. L'apport principal de cette proposition est de permettre l'étude de modèles qui sont hors de portée pour les outils de preuve purement automatiques, en intégrant une plus grande part d'expertise dans la description des modèles et et le raisonnement sur ces derniers. On s'intéressera tout particulièrement à la démonstration d'une condition suffisante sur les intéractions entre gènes pour la présence d'un unique état stable. A. Richard, "An extension of a combinatorial fixed point theorem of Shih and Dong", Advances in Applied Mathematics 41, 2008, 630-637. La description formelle sera effectuée en Coq, avec l'extension ssreflect déjà utilisée pour des résultats précédents en formalisation de concepts de biologie.
Le stage pourra être rémunéré. Le stage sera probablement co-encadré par Adrien Richard du laboratoire CNRS I3S.
recent work by Bernot, Comet, and Richard showed the advantages of formal methods for the understanding of systems biology. we want to pursue these investigations by bringing in proof systems like Coq. The main benefit is to address problems that are out of reach for purely automatic tools. We will concentrate on a sufficient condition for gene interactions to exhibit a single stable states (A. Richard, "an extension of a combinatorial fixed point theorem of Shih and Dong", Advances in Applied Mathematics 41, 2008, 630-637. The formal description will be encoded in the Coq system with the ssreflect extension that was already used for previous experiments in formalizing concepts from biology.
Partial supervision will probably be provided by A. Richard from the CNRS Laboratory I3S