Level of qualifications required : Bachelor's degree or equivalent
Fonction : Internship Research
About the research centre or Inria department
Located at the heart of the main national research and higher education cluster, member of the Université Paris Saclay, a major actor in the French Investments for the Future Programme (Idex, LabEx, IRT, Equipex) and partner of the main establishments present on the plateau, the centre is particularly active in three major areas: data and knowledge; safety, security and reliability; modelling, simulation and optimisation (with priority given to energy).
The 450 researchers and engineers from Inria and its partners who work in the research centre's 31 teams, the 100 research support staff members, the high-level equipment at their disposal (image walls, high-performance computing clusters, sensor networks), and the privileged relationships with prestigious industrial partners, all make Inria Saclay Île-de-France a key research centre in the local landscape and one that is oriented towards Europe and the world.
This researchinternship is offered at Inria Saclay IdF (https://www.inria.fr/en/centre/saclay) in the LIFEWARE project-team (http://lifeware.inria.fr). This team works in computational systems biology and develops the Biochemical Abstract Machine (BIOCHAM http://lifeware.inria.fr/biocham4) software for modeling, analyzing and synthesizing biochemical reaction networks (CRNs) using methods from fundamental computer science and mathematics. The software developments are expected to be integrated in BIOCHAM.
The internship will be supervised by François Fages and Sylvain Soliman.
Boolean SAT constraint solvers have shown outstanding performance for circuit and program proofing. The need to reason on data structures richer than Booleans has led to generalize them to SAT modulo Theories solvers, by combining SAT resolution techniques with other arithmetic or other constraint solving techniques, such as: programming linear, interval arithmetic, constraint programming.
In particular, the SAT solvers modulo differential equations, make it possible to reason about the continuous dynamics of a solution system of differential equations when the values of parameters or the initial values are not known precisely but are given in a range of values.
The following founding works
- 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 Gao Soonho Sicun Kong Edmund Clarke. arXiv: 1310.8278v1 [cs.LO] Oct 30, 2013
led to implementations (eg dReal system) that proved accessibility properties in parametric hybrid systems.
These results are particularly interesting in the contexts of computational systems biology or synthetic biology, because in these systems the parameters of the biochemical reaction systems are not precisely known and subject to strong variations.
The subject of the internship is to evaluate these techniques in the context of chemical reaction systems compared to the bounded model-checking techniques implemented in BIOCHAM
Our previous work on this topic is described in
- Aurélien Rizk, Grégory Batt, François Fages, Sylvain Soliman. Continuous Valuations of Temporal Logic Specifications with applications to Parameter Optimization and Robustness Measures. Theoretical Computer Science, 412(26):2827–2839, 2011. [ preprint ]
The trainee will have the task of testing the existing SAT modulo ODE systems, and evaluating them on the examples of biological systems that we treat in the team with BIOCHAM.
BIOCHAM being interfaced to the solver SAT Glucose and being implemented in Prolog with constraints having the arithmetic of intervals, an integration of SAT modulo ODE is possible in BIOCHAAm if necessary.
This subject requires a pronounced taste common and basic knowledge in algorithmics, programming and numerical integration of differential equations.
Specific knowledge about SAT solvers, constraint programming, Prolog, or systems biology will be a plus.
- Subsidised catering service
- Partially-reimbursed public transport
- Social security
- Paid leave
- Flexible working hours
- Sports facilities
- Theme/Domain : Algorithmics, Computer Algebra and Cryptology
- Town/city : PALAISEAU
- Inria Center : CRI Saclay - Île-de-France
- Starting date : 2019-04-01
- Duration of contract : 6 months
- Deadline to apply : 2019-09-30
The keys to success
We are seeking a highly talented and motivated candidate not afraid by crossing disciplinary frontiers.
Inria, the French national research institute for the digital sciences, promotes scientific excellence and technology transfer to maximise its impact. It employs 2,400 people. Its 200 agile project teams, generally with academic partners, involve more than 3,000 scientists in meeting the challenges of computer science and mathematics, often at the interface of other disciplines. Inria works with many companies and has assisted in the creation of over 160 startups. It strives to meet the challenges of the digital transformation of science, society and the economy.
Instruction to apply
Send an e-mail with CV + cover letter to Mr François Fages : françois.firstname.lastname@example.org
Defence Security :
This position is likely to be situated in a restricted area (ZRR), as defined in Decree No. 2011-1425 relating to the protection of national scientific and technical potential (PPST).Authorisation to enter an area is granted by the director of the unit, following a favourable Ministerial decision, as defined in the decree of 3 July 2012 relating to the PPST. An unfavourable Ministerial decision in respect of a position situated in a ZRR would result in the cancellation of the appointment.
Recruitment Policy :
As part of its diversity policy, all Inria positions are accessible to people with disabilities.
Warning : you must enter your e-mail address in order to save your application to Inria. Applications must be submitted online on the Inria website. Processing of applications sent from other channels is not guaranteed.