Rémi Delmas

Research Interests

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.

Phd Students

• 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.

Papers

You can find some of my papers on DBLP.

Tools

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).

,

Previous experience

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.

,