2019-01283 - Boolean SATisfiability modulo Differential Equations for verifying chemical reaction networks

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.

Context

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.

Assignment

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

Main activities

Our previous work on this topic is described in

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.

Skills

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.

Benefits package

  • Subsidised catering service
  • Partially-reimbursed public transport
  • Social security
  • Paid leave
  • Flexible working hours
  • Sports facilities

Remuneration

500 euros/month