Internships /
Sujets de Stages de Grandes Ecoles et Master
 
2011-2012
EPI Contraintes
INRIA Paris-Rocquencourt.


These internships of 3 to 6 months are of course remunerated. Most of these topics can be continued in a PhD Thesis programme.


Title: Representation of hybrid systems by ordinary differential equations plus events.

Theme: Automata theory

Laboratory:
INRIA Paris-Rocquencourt
Domaine de Voluceau 78150 Rocquencourt

Team: EPI Contraintes

Supervisor: François Fages Francois.Fages@inria.fr

General presentation:
Hybrid systems are dynamical systems which combine both discrete and continuous dynamics. Many numerical simulation and analysis tools permit to mix ordinary differential equations (ODE) with events which dynamically change the values of some parameters or variables once a condition is satisfied. This is for instance the case of the XPPAUT system [1] for analyzing dynamical systems, of the Systems Biology Markup Language [2] for modeling biological processes, and of the Biochemical Abstract Machine Biocham [3] for simulating and analyzing SBML models. This event mechanism has often been introduced for practical reasons to deal with particular cases and is marginally used, however it provides the full expressive power of hybrid automata [4].

Objectives:
The subject of this internship is to design an interface for representing hybrid automata on top of SBML/Biocham reaction rules and events, and to investigate their expressive power for multi-scale modeling on the one hand, and for designing and implementing hybrid stochastic-differential simulators on the other hand.

Bibliography:
[1] Bard Ermentrout. Simulating, Analyzing, and Animating Dynamical Systems: A Guide to XPPAUT for Researchers and Students. SIAM, 2002.

[2] The Systems Biology Markup Language SBML. http://sbml.org

[3] Biocham web page and reference manual. http://contraintes.inria.fr/biocham/

[4] Thomas Henzinger. The theory of hybrid automata.

Skills:
Formal methods in computer science
Numerical analysis
Interest for systems biology


Title: Model reductions: from graph theory to dynamics.

Theme: Bioinformatics

Laboratory:
INRIA Paris-Rocquencourt
Domaine de Voluceau 78150 Rocquencourt

Team: EPI Contraintes

Supervisor: François Fages Francois.Fages@inria.fr

General presentation:
In the study of dynamical systems modeled with ordinary differential equations, model reductions are traditionally based on a separation of time scales which allow for a reduction of the dimension of the system. In the context of systems biology and the comparison of large networks of biochemical reactions, we have designed a graph-theoretic method to reduce reaction graphs by deleting and merging species and reaction vertices [1]. The existence of such a graph transformation for reducing a source graph G1 to a target graph G2 is in turn equivalent to the existence of a subgraph epimorphism (SEPI) from G1 to G2. This general notion of model reduction has proven effective to organize model repositories like biomodels.net in hierarchies of models related by reduction/refinement relationships.

Objectives:
The subject of this internship is to study kinetic expressions for the reduced/refined models and kinetic conditions for these reductions, such as for instance, species deletions for species in excess, reaction deletions for slow reverse reactions, species mergings for fast equilibria (QSSA) [2], reaction mergings for limiting reactions [3].

Bibliography:
[1] Steven Gay, Sylvain Soliman, François Fages: A graphical method for reducing and relating models in systems biology. Bioinformatics 26(18):575-581 (2010)

[2] L. Segel. Modeling Dynamic Phenomena in Molecular and Cellular Biology. Cambridge University Press (March 30, 19

[3] O.Radulescu, A.N.Gorban, A.Zinovyev, A.Lilienbaum, "Robust simplifications of multiscale biochemical networks", BMC
Systems Biology, 2008, 2:86.

Skills:
Graph theory
Numerical analysis
Interest for systems biology


Title: Theory of temporal logic constraint solving

Theme: Logic

Laboratory:
INRIA Paris-Rocquencourt
Domaine de Voluceau 78150 Rocquencourt

Team: EPI Contraintes

Supervisor: François Fages Francois.Fages@inria.fr

General presentation:
Temporal logics were introduced by Pnueli in 1977 for reasoning about computer programs and verifying safety and liveness properties. Efficient model-checking techniques have been developed since for verifying circuits and programs. Model-checking can be generalized to temporal logic constraint solving, by considering temporal logic formulae with free variables over some domain D, and by computing a validity domain for the variables rather than a truth value for the formula [1]. This allows us to define a continuous degree of satisfaction for a temporal logic formula in a given structure, opening up the field of
model-checking to optimization [2].

Objectives:
The subject of this internship is to establish the links between temporal logic constraint solving [1] and the theory and implementations of satisfiability modulo theories [3].


Bibliography:
[1] F.Fages and A.Rizk. From Model-Checking to Temporal Logic Constraint Solving.Proc of 15th International Conference on Principles and Practice of Constraint Programming, CP'09. LNCS, Springer-Verlag. 2009.

[2] A.Rizk, G.Batt, F.Fages, S.Soliman. Continuous Valuations of Temporal Logic Specifications with Applications to Parameter Optimization and Robustness Measures. Theoretical Computer Science, 2011

[3] Nieuwenhuis, R.; Oliveras, A.; Tinelli, C. Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T). Journal of the ACM, 53, pp. 937–977, 2006.


Skills:
Formal methods in computer science
Logic
Constraint programming
Interest for systems biology


Title: Patterns of quantitative temporal logic formulae for systems biology

Theme: Logic

Laboratory:
INRIA Paris-Rocquencourt
Domaine de Voluceau 78150 Rocquencourt

Team: EPI Contraintes

Supervisor: François Fages Francois.Fages@inria.fr

General presentation:
Systems biology is an interdisciplinary research field which aims at elucidating and mastering the complexity of biological processes in terms of their elementary interactions. Formal methods from computer science have been used with success to reason on large regulatory networks by applying both static analyses tools such as abstract interpretation for instance and dynamical analysis tools such as temporal logic and model-checking techniques [1]. A modeling environment like Biocham [2] is composed of a rule-based language for modeling biochemical systems (compatible with SBML) with several simulators (boolean, differential, stochastic), and a temporal logic based language to formalize the temporal properties of a biological system and validate models with respect to such specifications, with unique features for developing/correcting/completing/coupling models, including the inference of kinetic parameters in high dimension from temporal logic constraints [3].

Objectives:
The aim of this internship is to develop a set of patterns of quantitative temporal logic formulae (similarly to what has been done for Boolean temporal logic in [4]) and to apply them systematically for the analysis of dynamical models of biological processes at the cellular level. These patterns will be used to automatically generate quantitative temporal specifications of numerical data time series and models (through simulation). These specifications will be used in a number of manners including model reductions, testing, parameter search, robustness and sensitivity analyses etc.


Bibliography:
[1] F.Fages, S. Soliman. Formal Cell Biology in BIOCHAM (tutorial). 8th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Computational Systems Biology. In memory of Nadia Busi. Bertinoro, Italy. Springer-Verlag, LNCS 5016, 2008.

[2] Biocham web page and reference manual. http://contraintes.inria.fr/biocham/

[3] A.Rizk, G.Batt, F.Fages, S.Soliman. Continuous Valuations of Temporal Logic Specifications with Applications to Parameter Optimization and Robustness Measures. Theoretical Computer Science, 2011

[4] Pedro T. Monteiro, Delphine Ropers, Radu Mateescu, Ana T. Freitas and Hidde de Jong. Temporal logic patterns for querying dynamic models of cellular interaction networks. Bioinformatics, Volume24, Issue 16:227-233

Skills:
Formal methods in computer science
Mathematical logic
Interest for systems biology

Title
Refactoring of the BIOCHAM software using modular Constraint Logic Programming
Theme
Programming Languages
Laboratory
INRIA Paris-Rocquencourt
Domaine de Voluceau 78150 Rocquencourt
Team
EPI Contraintes
Supervisor
François Fages Francois.Fages@inria.fr and Sylvain Soliman Sylvain.Soliman@inria.fr
General presentation

Systems biology is an interdisciplinary research field which aims at elucidating and mastering the complexity of biological processes in terms of their elementary interactions. A modeling environment like BIOCHAM [1, 2] is composed of a rule-based language for modeling biochemical systems (compatible with SBML) with several simulators (boolean, differential, stochastic), and a temporal logic based language to formalize the temporal properties of a biological system and validate models with respect to such specifications, with unique features for developing/correcting/completing/coupling models, including the inference of kinetic parameters in high dimension from temporal logic constraints [3].

BIOCHAM is currently written mainly in GNU Prolog, and is the result of years of development by several contributors. Unfortunately, GNU Prolog does not offer any module system, nor any testing or documentation framework. The work done in the team on the EMoP language [4] should allow to refactor or rewrite the core of BIOCHAM in a much more satisfactory way with respect to current best practices in Software Engineering. Along the way, this use of EMoP will allow to enrich the available libraries of the language.

Objectives
The aim of this internship is to rewrite the core functions of the BIOCHAM software using state of the art techniques in maintainable software engineering (Test Driven Development, Automatic Documentation generation, etc.) and based on the modular extension of GNU Prolog provided by EMoP
Bibliography
  1. BIOCHAM web page and reference manual.
  2. F.Fages, S. Soliman. Formal Cell Biology in BIOCHAM (tutorial). 8th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Computational Systems Biology. In memory of Nadia Busi. Bertinoro, Italy. Springer-Verlag, LNCS 5016, 2008.
  3. A.Rizk, G.Batt, F.Fages, S.Soliman. Continuous Valuations of Temporal Logic Specifications with Applications to Parameter Optimization and Robustness Measures. Theoretical Computer Science, 2011
  4. Rémy Haemmerlé, François Fages, and Sylvain Soliman. Closures and modules within linear logic concurrent constraint programming. In V. Arvind and Sanjiva Prasad, editors, Proceedings of FSTTCS 2007, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, volume 4855 of Lecture Notes in Computer Science, pages 544-556. Springer-Verlag, 2007
Skills
  • Constraint Logic programming
  • Software Engineering (Test Driven Development, Documentation generation, Refactoring techniques, etc.)
  • Interest for systems biology
Title
Automatic generation of Graphical User Interface using modular Constraint Logic Programming and end-user documentation
Theme
Programming Languages
Laboratory
INRIA Paris-Rocquencourt
Domaine de Voluceau 78150 Rocquencourt
Team
EPI Contraintes
Supervisor
François Fages Francois.Fages@inria.fr and Sylvain Soliman Sylvain.Soliman@inria.fr
General presentation

Systems biology is an interdisciplinary research field which aims at elucidating and mastering the complexity of biological processes in terms of their elementary interactions. A modeling environment like BIOCHAM [1, 2] is composed of a rule-based language for modeling biochemical systems (compatible with SBML) with several simulators (boolean, differential, stochastic), and a temporal logic based language to formalize the temporal properties of a biological system and validate models with respect to such specifications, with unique features for developing/correcting/completing/coupling models, including the inference of kinetic parameters in high dimension from temporal logic constraints [3].

The current Graphical user Interface (GUI) of the BIOCHAM modelling environment is well separated from its core functionalities but so much separated that it has become a burden to maintain. The EMoP language [4] brings to Constraint Logic Programming a notion of modules that has a well defined meaning in the logical semantics. Along with those modules come interfaces which could be used in the same way as types in the functional paradigm to automatically derive possible widgets in a GUI [5]. Moreover, the User Manual provides a structuration of the available commands in BIOCHAM. Combining these two points should allow to obtain an automatically generated GUI for BIOCHAM.

Objectives
The aim of this internship is to study the possibility to generate automatically (some parts of) the GUI of BIOCHAM using:
  • the EMoP interface of modules to specify widgets to use, in a similar way to what is done for Haskell in Autoform [5]
  • the User Manual to define widgets groupings
The question of whether the EMoP interfaces are well suited to this task will also be at the heart of the study.
Bibliography
  1. BIOCHAM web page and reference manual.
  2. F.Fages, S. Soliman. Formal Cell Biology in BIOCHAM (tutorial). 8th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Computational Systems Biology. In memory of Nadia Busi. Bertinoro, Italy. Springer-Verlag, LNCS 5016, 2008.
  3. A.Rizk, G.Batt, F.Fages, S.Soliman. Continuous Valuations of Temporal Logic Specifications with Applications to Parameter Optimization and Robustness Measures. Theoretical Computer Science, 2011
  4. Rémy Haemmerlé, François Fages, and Sylvain Soliman. Closures and modules within linear logic concurrent constraint programming. In V. Arvind and Sanjiva Prasad, editors, Proceedings of FSTTCS 2007, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, volume 4855 of Lecture Notes in Computer Science, pages 544-556. Springer-Verlag, 2007
  5. Gracjan Polak, Janusz Jarosz. Automatic Graphical User Interface Form Generation Using Template Haskell. TFP 2006, Seventh Symposium on Trends in Functional Programming, University of Nottingham, UK, 19 - 21 April, 2006.
Skills
  • Constraint Logic programming
  • Software Engineering (Test Driven Development, Documentation generation, Refactoring techniques, etc.)
  • Interest for systems biology
Title
Efficient compilation for an angelic programming language
Theme
Programming Languages
Laboratory
INRIA Paris-Rocquencourt
Domaine de Voluceau 78150 Rocquencourt
Team
EPI Contraintes
Supervisor
François Fages Francois.Fages@inria.fr and Sylvain Soliman Sylvain.Soliman@inria.fr
General presentation

The SiLCC programming language is currently developed as a prototype implementation, as close as possible to the theoretical LCC framework [1] of Linear Concurrent Constraint programming. Among its features, the angelic semantics call for a new coding of constraint propagators and novel views of the derivation tree, for instance as derivation nets [2].

Objectives
The aim of this internship is to work on the efficient compilation of the SiLCC language, and notably to measure that by implementing a simple Finite Domain propagator in SiLCC. The current compiler is written in OCaml and relies on an LLVM back-end, but these choices might be changed if some better tools are found.
Bibliography
  1. François Fages, Paul Ruet, and Sylvain Soliman. Linear concurrent constraint programming: operational and phase semantics. Information and Computation, 165(1):14–41, 2001. doi:10.1006/inco . 2000.3002
  2. Thierry Martinez, Design and implementation of a concurrent programming language with constraints in linear logic , Doctoral Consortium of International Logic Programming Conference, Edinburgh (United Kingdom), 2010
Skills
  • Compilation
  • LLVM or similar frameworks
  • Constraint Logic programming

More to come ...