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


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


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.


Academic Curriculum

In 2004 I obtained a PhD in computer science from the ISAE doctoral school. My PhD grant was financed and hosted by ONERA/DTIM where I work now.

My PhD resarch addressed the design of a formal meta-logical framework based on category theory for the modelling and verification of integrated modular avionics systems (IMA), unifying domain oriented views and properties of the system: functional correctness, real time performance, fault tolerance; allowing to compose results of analyses performed in each view using for instance the lesar Model-Checker for Lustre for functional properties, the UPAAL model checker for real-time properties,  and minimal cutset generators for safety assessment.

Between 2000 and 2001 I was a post-graduate computer science student at RMIT in Melbourne, Australia, specializing in real-time physics-based 3D animation (hosted at RMIT's Interactive Information Institute "I cubed").

In 2000 I obtained an aerospace engineering dergee from ENSMA, with a major in Industrial computer systems and formal methods.