Involved in the development of Asterios Technologies’ main product (Core Team), consisting of a compiler for the PsyC language (written in C++) and a real-time operating system (written in C) by implementing various functionalities such as the fault and error management service.
Designed a formal verification methodology (as part of my CIFRE PhD supervised by Inria) as well as a prototype formal verification tool (written in OCaml) for the PsyC language based on state-of-the-art symbolic model-checking along with an optimization procedure to speed-up verification time by up to 95% compared to a naive approach.
Previously involved in the development of a tool (written in Python) that performs the validation of compilations performed by the Asterios compiler (Checker Team) by implementing the tool’s frontend (parser and graph analysis), in a context of avionics certification (DO-178)
Contributed to a technical audit by analyzing Asterios features using HAZOP risk and failure analysis methodology.
(Co-)Supervised 3 trainees over the years on topics such as Lingua Franca to PsyC translation and random PsyC code generation, which led to the discovery of 9 bugs in the Asterios toolchain.