2019-01283 - SATisfaisabilité booléenne modulo Equations Différentielles pour vérifier les réseaux de réactions chimiques

Niveau de diplôme exigé : Bac + 3 ou équivalent

Fonction : Stagiaire de la recherche

A propos du centre ou de la direction fonctionnelle

Le centre de recherche Inria Saclay – Île-de-France, créé en 2008, accueille 450 scientifiques et 100 membres des services d’appui à la recherche. Les scientifiques sont organisés en 35 équipes de recherche dont 26 sont communes avec des partenaires du plateau de Saclay.

Le centre Inria Saclay - Île-de-France est un acteur essentiel de la recherche en sciences du numérique sur le plateau de Saclay. Il porte les valeurs et les projets qui font l’originalité d’Inria dans le paysage de la recherche : l’excellence scientifique, le transfert technologique, les partenariats pluridisciplinaires avec des établissements aux compétences complémentaires aux nôtres, afin de maximiser l’impact scientifique, économique et sociétal d’Inria.

Contexte et atouts du poste

Ce stage de recherche est proposé chez Inria Saclay IdF (https://www.inria.fr/fr/centre/saclay) dans l'équipe-projet LIFEWARE (http://lifeware.inria.fr). Cette équipe travaille en biologie des systèmes computationnels et développe le logiciel Machine Abstraite Biochimique (BIOCHAM http://lifeware.inria.fr/biocham4) pour la modélisation, l'analyse et la synthèse des réseaux de réactions biochimiques (CRN), en utilisant des méthodes issues de l'informatique fondamentale et des mathématiques. Les développements logiciels auront vocation à être intégrés dans  BIOCHAM.

Le stage sera encadré par François Fages et Sylvain Soliman.

Mission confiée

Les solveurs de contraintes booléennes SAT ont montré des performances remarquables pour la preuve de circuits et de programmes. Le besoin de raisonner sur des structures de données plus riches que les booléens a conduit à les généraliser à des solveurs SAT modulo Théories, en combinant les techniques de résolution SAT à d'autres techniques de résolution de contraintes arithmétiques ou autres, telles que: programmation linéaire, arithmétique d'intervalles, programmation par contraintes.

En particulier, les solveurs SAT modulo équations différentielles, permettent de raisonner sur la dynamique continue d'un système solution d'équations différentielles lorsque les valeurs de paramètres ou les valeurs initiales ne sont pas connues précisémment mais sont données dans un intervalle de valeurs.

Les travaux fondateurs suivants

  • A. Eggers, M. Franzle, and C. Herde. SAT modulo ODE: A direct SAT approach to hybrid systems. In Proc. of ATVA’08, LNCS 5311, pp. 171–185, 2008.
  • Satisfiability Modulo ODEs Sicun Gao Soonho Kong Edmund Clarke. arXiv:1310.8278v1 [cs.LO] 30 Oct 2013

ont conduit à des implémentations (ex. système dReal) qui ont permis de prouver des propriétés d'accessibilité dans les systèmes hybrides paramétrés.

Ces résultats sont particulièrement intéressants dans les contextes de la biologie calculatoire des systèmes ou de la biologie synthétique, car dans ces systèmes les paramètres des systèmes de réactions biochimiques ne sont pas connus précisément et sujets à de fortes variations. Le sujet du stage est d'évaluer ces techniques dans ce contexte comparativement aux techniques de model-checking bornée implémentées dans BIOCHAM

 

 

Principales activités

Notre travail antérieur sur ce sujet est décrit dans

Le stagiaire aura pour mission d'essayer les systèmes SAT modulo ODE existants, et de les évaluer sur les exemples de systèmes biologiques que nous traitons dans l'équipe avec BIOCHAM.

BIOCHAM étant interfacé au solveur SAT Glucose et étant implémenté en Prolog avec contraintes disposant de l'arithmétique d'intervalles, une intégration d'algorithme SAT modulo ODE est envisageable dans BIOCHAAm si besoin.

 

Compétences

Ce sujet nécessite des connaissances communes et de base en algorithmique,  programmation, et intégration numérique des équations différentielles.

Des connaissances spécifiques sur les solveurs SAT, la programmation par contraintes, Prolog, ou la biologie des systèmes seront un plus.

Avantages

  • Restauration subventionnée
  • Transports publics remboursés partiellement
  • Sécurité sociale
  • Congés payés
  • Aménagement du temps de travail
  • Installations sportives

Rémunération

Gratification : environ 500 euros/mois