I joined ONERA in 2009. My research focuses on the integration of SAT, MaxSAT and SMT solvers at various levels of the development process for critical embedded systems:
- At the architectural level:
- Safety assessment and fault-tolerant design using model based techniques:
- Verification of application mapping safety (IMA modules) and communication mapping safety (AFDX networks).
- IMA application deployment synthesis and optimization under safety, functional and real-time constraints using SAT and MaxSat solvers.
- At the software level :
- critical synchronous software modelling and verification using SAT and SMT-based techniques.
I sometimes venture out of embedded systems (see project deontic information diffusion policies below).
I have been or am currently involved in the following projects (in inverse chronological order):
- 2012-2016: CAFEIN ANR project: IC3/PDR formal verification algorithms for synchronous programs (Lustre, Scade)
- 2011-2015: PR MAPEIS (internal project): creating a formal specification language and associated SMT-based model-cheker dedicated to the expression and verification of information sharing policies, in the context of European space situation awareness (a system of systems).
- 2011-2014: PR SCC (internal project): Allocating tasks to cores and communication links in the Network On Chip in the Intel 48-cores SCC processor, while minimizing network congestion and communication latency, using MaxSAT techniques.
- 2010-2012 OGRE project (Airbus): Automatically routing and optimizing the wiring of aircraft sensors under safety constraints, while minmizing the weight of the wiring.
- 2009-present PAM (DGAC+Airbus), PR MAUSART (interal) projects : Supporting the design space exploration of Integrated Modular Avionics applications and platforms under safety and real-time constraints, using SAT and MaxSAT techniques.
- 2009-present PAM (DGAC+Airbus), PR MAUSART (internal) projects: Automatically allocating tasks to IMA computing modules while optimizing the routing of VirtualLinks in the AFDX network, under safety constraints, using MaxSAT techniques.
- 2009 - 2011 : MISSA FP-7 project (European Union): Allocating DAL levels and failure probability budgets to aircraft functions, and selectively downgrading DAL levels in coherence with ARP-4754 guidelines, by taking into account the way in which the failure modes are combined in a given set of Failure Conditions, using MaxSAT and linear programming techniques.
- 2014-2017: with Claire Pagetti, advising PhD student Kevin Delmas, on the topic of evaluating multi- and many-core processors for safety critical real-time embedded applications and designing a suitable development chain, taking into account safety, functional and real-time requirements from high-level application design to code generation for the multi/many-core target to verification/validation (of course, SAT and/or SMT solvers will be used at some point in this thesis).
- 2011-2014: advising Adrien Champion, on the topic of proving properties of synchronous dataflow programs by combining various SMT-based techniques such as k-induction, quantifier elimination, numerical lemma generation using polyhedral computations, property directed reachability analysis, etc.
You can find some of my papers on DBLP.
I contribute the development of, or am the main author of the following software tools :
- TUFF: an smt-based parallel model checker for synchronous transition systems, including k-induction, quantifier elimination and numerical lemma generation heuristics;
- SMT-QE: a tool for efficient SMT-based quantifier elimination for quantifier free first order formulas mixing boolean, linear real and integer arithmetic theories;
- DALculator: a MaxSAT-based tool for automatic independence requirements generation, automatic allocation of Development Assurance Levels (DALs) and allocation of failure probability budgets to IMA functions, based on minimal cut sets information;
- Peps & Peps-analyzer: a formal language an associated SMT-based property prover for deontic information sharing policies;
- eLogical: A grounder for many-sorted first order logic formulas interpreted over finite domains to pure SAT, used for various tasks inside ONERA (task mapping, communication routing, scheduling, etc.).
(Links to be added soon).