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).
Before joining ONERA, from 2005 to 2009, I was employed by Prover Technology and in charge of designing and developping advanced SAT-based formal verification techniques for SIL-4 railway control applications (interlocking and real-time train control), known as Prover Certifier solutions. In particular, I developped the SIL-4 certifiable SAT-based equivalence (ie, bisimulation) checker for sequential boolean circuits.
While there, I also held the technical manager position for Ansaldo-STS (FR), Invensys-Westinghouse (UK), Airbus (FR), and maintained the SCADE Desgin Verifier Plug-In.
I was also briefly in charge of client prospection in the UK, of pre-sale technical feasibility studies, and the manager of a small agile validation team for SIL-4 grade software verification solutions.