I'm looking for challenges that require a holistic view: gathering functional requirements, translate them into a technical roadmap and into a comprehensive architecture, especially if it has to embrace different kinds of technologies. All this with a high expectation on quality: development best practices, tests, etc.

Professional Experience

  • Tech Lead EasyMile 2017
    • Ensure overall consistency of the vehicle stack (from the embedded hardware to the fleet management servers)
    • Cybersecurity technical referent: work with Safety team and domain experts to design a secure autonomous vehicle
    • Technical management of cross-teams projects
    • Management of IT and Operations (6 persons) to sustain the rapid company growth
    • Design a framework for the technical assessment of candidates; more than 100 interviews conducted: C, C++, Elixir, software design, etc.
  • R&D software engineer EasyMile 2015 - 2017
    • Maintenance of a LIDAR driver and autonomous vehicles-related algorithms (C++11)
    • Specification, design and implementation of autonomous vehicles state machines (C++11, Boost.MSM)
    • Specification and design of a stateless protocol to interact with autonomous vehicles (Protocol Buffers, TLS); implementation of the server (Elixir); implementation of the client on vehicles (C++11, Boost.ASIO)
    • Technical expertise for modern C++ developpment (sanitizers, good practices, etc.)
    • Technical assessment of candidates
  • Engineer, Researcher & Teacher ISAE 2012 - 2015
    • Research in formal verification (model checking), a CPU and memory intensive task.
    • Development of a generic library (C++14, Boost) for decision diagrams, a data structure which gives the possibility to work on compressed data without decompressing it.
    • Development of a high performance model checker (C++14, Boost) for Petri nets.
    • Technical lead for a Java application dedicated to networks optimization.
    • Teaching (software engineering, C, Python), internships supervision.
    • C++ training (moving to C++11/14, software engineering, parallel programming)
  • R&D software engineer Quanthouse 2011 - 2012
    • Maintenance and optimization of a C++ low-latency middleware.
  • Post-doctoral researcher LAAS/CNRS 2010 - 2011
    • The LAAS laboratory develops TINA, a model checking tool. As such, it is a CPU and memory intensive tool. Part of my work was to improve this situation using on-disk databases and compression with decision diagrams.
    • One of the modeling language recognized by TINA is Fiacre which a compiler pre-process, generating C code and Petri nets. An other part of my work was to improve the generated code and the associated runtime.
  • Ph.D. student LIP6 2006 - 2009
    • See Education section for research activities
    • Deployment and administration of a collaborative environment for the whole laboratory (SVN/Trac/BuildBot).
    • Applied and theoretical teachings for classes of 30 to 200 students. Some courses: Introduction to Middlewares; Distributed Systems Engineering (project life: from inception to implementation); Automata Theory.
    • Organization of an international conference (200 persons)
    • Supervision of 14 internships, undergraduate and graduate.
    • iOS training for LIP6 members

Some open-source projects

  • protox library for Protocol Buffers Elixir

    Protocol buffers are Google's language-neutral, platform-neutral, specification for data serialization. While Google provides implementations for a lot of languages, Elixir is not one of them. Protox is a pure Elixir implementation of Protocol Buffers: written using meta-programming, it provides very good performances and expose data with standard structures.

  • netcode library for Network Coding C++11

    Network coding is a technique to improve network efficiency through the usage of redundancy packets to avoid retransmissions. Netcode is a library which implements network coding using Galois fields. It provides C bindings.

  • pnmc efficient model checker for Petri nets C++14

    Model checkers are a category of tools that automatically explore all the states of a system, given a formal description, to verify properties (e.g. "Does my system have a deadlock?"). It's a memory and CPU intensive process, making C++ the right language. This tool features parsers for several Petri net formats, JSON and DOT export of results; it relies on the Boost libraries to provide portability.
    This tool had the second place at the Model Checking Contest (2014 and 2015 editions). On all given systems' descriptions ("models"), it was the tool with the smallest memory footprint on 50% of models, and was the fastest on 75% of the models. All in all, it was the tool which was able to handle the maximum number of models.

  • libsdd generic library for decision diagrams C++14

    This library is an implementation of the Hierarchical Set Decision Diagram (SDD) data structure. SDDs provide the ability to store arbitrary types, making this structure a generic one. C++ templates are a natural way of implementing SDDs, thus providing efficient and generic algorithms. It features a custom reference-counted garbage collector, which is required by the nature of decision diagrams, and a custom tagged union (like Boost.Variant) to provide a fast and safe visitor mechanism. Also, it uses type traits, whenever possible, to statically choose the best algorithms at compile time. Finally, great care is taken to allocate and use memory in a contiguous way to ensure caches are used at their best.

Education

  • 2009 Ph.D. in Computer Sciences with highest honors Paris 6

    Model checking is a technique of verification which has the major advantage of being fully automatic. However, the model checking process exhaustively explores the states of the analyzed models. This causes a major problem: combinatorial explosion due to the state spaces of large systems, which can easily have more than 10100 states.

    This thesis offers two types of solutions to address more effectively larger spaces of states. The first relies on the resources of parallel machines with multiple CPUs or multi-core and those of clusters, achieving linear speedups. The second solution deals with Hierarchical Set Decision Diagrams (an enhancement of the Binary Decision Diagrams) by automating and generalizing a technique called "saturation", whose empirically shown effectiveness (in orders of magnitude) is very difficult to achieve manually.

    Dissertation (fr)   Defense (fr)

  • 2006 M.Sc. in Computer Sciences with honors Paris 6

    This degree is a specialization in "Distributed Systems Engineering". It covers topics such as: conception, modeling and formal verification of parallel and distributed systems; metamodeling; code generation; distributed algorithms.

Skills

Languages

  • Proficient: C++11/14/17, Elixir
  • Strong knowledge: C, Standard ML, Python
  • Basic knowledge: Shell scripting, Java

Some tools and environments

  • C++: GCC, Clang, Boost, meta-programming, ...
  • Compilation and packaging: autotools, make, CMake
  • Collaborative work: SVN, Git, JIRA
  • Modeling: UML, AADL, Petri nets
  • Parallelism: POSIX threads, Threading Building Blocks, C++11/14 standard library
  • Network: UNIX sockets, Boost.ASIO
  • OS: Any UNIX-like system, daily usage of MacOS X and Linux

Bibliography