Nicolas “Niols” Jeannerod

Top

Curriculum Vitæ

(You can also get this curriculum vitæ as PDF.)

Career

2021—now Consultant at Tweag/Modus Create. I joined Tweag in September 2021, which was then acquired by Modus Create in June 2022. Tweag/Modus Create is a consultancy specialised, as far as I am concerned, in functional languages (most notably OCaml and Haskell) and Nix/NixOS. I have, since I joined, worked in very different contexts, with very different people, on very different projects. In addition to client work, I am a squad lead internally, mentoring fellow engineers as well as following them and communicating on their behalf to other instances of the company.
2024—now Software auditor at Tweag/Modus Create. In August 2024, in parallel to my work on the Fediversity project, I started periodically running code audit for codebases in OCaml or Haskell. Those vary drastically in scope, but some have been security audits for web applications, in which case I am paired with a security auditor of Modus Create.
2024—now Nix engineer at Tweag/Modus Create. In September 2024, I joined the Nix team at Tweag and started working on the Fediversity project. This project, supported by NLnet, consists on my part in the development of NixOS modules to ease the deployment of clusters of machines serving e-mail and Fediverse software, among other things, to thousands of users.
2023—2024
(13 months)
Haskell engineer at Tweag/Modus Create. From July 2023, with a team of Haskell engineers from Modus Create, we enhanced the consensus algorithm of the Cardano blockchain, creating tooling to run richer and more complex tests than what existed before, and addressing the vulnerabilities of nodes joining or rejoining the network. This effort terminated during the summer 2024 and the new algorithm, going by the sweet name of Ouroboros Genesis, is in the process of being deployed in Cardano nodes.
2022—2023
(8 months)
Research software engineer at Tweag/Modus Create. Following my work with Hachi, I joined the internal High Assurance Software group in September 2022, where I worked towards a similar purpose on a different tool suite written in Haskell: I helped develop Pirouette and Cooked Validators.
2021—2022
(12 months)
Research software engineer at Tweag/Modus Create. In September 2021, shortly after starting my work at Tweag, I joined Hachi, an R+D effort by MELD aiming at building a dynamic analysis tool suite for smart contracts on Cardano, mostly in Racket. I was mostly working on the concolic execution of smart contracts and on a DSL to specify expectations of such contracts. The effort was discontinued in August 2022.
2017—2021
(3½ years)
PhD in Computer Science at IRIF (Université de Paris, France) with Ralf Treinen and Yann Régis-Gianas on the “Verification of Shell Scripts Performing File Hierarchy Transformations”. This involved a more theoretical side working on extending feature tree logics and working on their decidability; and a more practical side implementing the actual analysis tooling, from a parser of Shell to a satisfiability solver for formulas in our logics. This effort led to the report of over 150 bugs on Debian packages.
2013—2017
(4 years)
ENS Graduate Degree at the École normale supérieure (Paris, France). This is a research-oriented four-year program including the third year of bachelor, the two years of master and an extra year — in my case, a one year-long internship. The degree requires the validation of extra courses in addition to the bachelor and master.
2014—2016
(2 years)
Master's Degree in Computer Science at the Université de Paris (France). The “Master Parisien de Recherche en Informatique” is a research-oriented master program in computer science whose purpose is to train future scientists through intensive exposure to contemporary research.
See more about my professional experience, my education or my PhD thesis.

Interests

Abstract I like specifications, abstraction and modularisation. I firmly believe in strongly typed functional programming, compilers, formal methods and program verification.
Concrete I enjoy working on low-level objects — network, systems or code optimisation, for instance. I am not afraid to dig into standards and RFCs.
Packaging I try to write good code, well designed and documented, used in practice.
System On my free time, I administrate a Debian server providing websites, email, cloud, etc.
Talks I love teaching and giving talks and I am said to be good at it.

Languages

Main OCaml, POSIX Shell Natural Fluent in French and English
Good Haskell, Racket, TeX/LaTeX OK Web, C, Java, Python, other Lisp

Outside of Work

Music I spend a lot of time playing music (piano & clarinet mostly, but I love trying all kind of instruments), writing music and typesetting music (with LilyPond).
SCD I also spend an awful lot of time doing Scottish Country Dancing. This includes dancing it, teaching it, playing music for it and organising local and international events.

Full Professional Experience

2021—now Consultant at Tweag/Modus Create. I joined Tweag in September 2021, which was then acquired by Modus Create in June 2022. Tweag/Modus Create is a consultancy specialised, as far as I am concerned, in functional languages (most notably OCaml and Haskell) and Nix/NixOS. I have, since I joined, worked in very different contexts, with very different people, on very different projects. In addition to client work, I am a squad lead internally, mentoring fellow engineers as well as following them and communicating on their behalf to other instances of the company.
2024—now Software auditor at Tweag/Modus Create. In August 2024, in parallel to my work on the Fediversity project, I started periodically running code audit for codebases in OCaml or Haskell. Those vary drastically in scope, but some have been security audits for web applications, in which case I am paired with a security auditor of Modus Create.
2024—now Nix engineer at Tweag/Modus Create. In September 2024, I joined the Nix team at Tweag and started working on the Fediversity project. This project, supported by NLnet, consists on my part in the development of NixOS modules to ease the deployment of clusters of machines serving e-mail and Fediverse software, among other things, to thousands of users.
2023—2024
(13 months)
Haskell engineer at Tweag/Modus Create. From July 2023, with a team of Haskell engineers from Modus Create, we enhanced the consensus algorithm of the Cardano blockchain, creating tooling to run richer and more complex tests than what existed before, and addressing the vulnerabilities of nodes joining or rejoining the network. This effort terminated during the summer 2024 and the new algorithm, going by the sweet name of Ouroboros Genesis, is in the process of being deployed in Cardano nodes.
2022—2023
(8 months)
Research software engineer at Tweag/Modus Create. Following my work with Hachi, I joined the internal High Assurance Software group in September 2022, where I worked towards a similar purpose on a different tool suite written in Haskell: I helped develop Pirouette and Cooked Validators.
2021—2022
(12 months)
Research software engineer at Tweag/Modus Create. In September 2021, shortly after starting my work at Tweag, I joined Hachi, an R+D effort by MELD aiming at building a dynamic analysis tool suite for smart contracts on Cardano, mostly in Racket. I was mostly working on the concolic execution of smart contracts and on a DSL to specify expectations of such contracts. The effort was discontinued in August 2022.
2021 Member of the organising committee of CONFLANG, a workshop colocated with SPLASH in October 2021.
2017—2021
(3½ years)
PhD in Computer Science at IRIF (Université de Paris, France) with Ralf Treinen and Yann Régis-Gianas on the “Verification of Shell Scripts Performing File Hierarchy Transformations”. This involved a more theoretical side working on extending feature tree logics and working on their decidability; and a more practical side implementing the actual analysis tooling, from a parser of Shell to a satisfiability solver for formulas in our logics. This effort led to the report of over 150 bugs on Debian packages.
2016—2020
(4 years)
Teaching at UFR Informatique (Université de Paris, France) including both practical and written exercises sessions for a total of 240h over 4 years. In addition to these hours in front of the students, the work included preparing materials and grading exams and projects.
2017
(3 months)
Google Summer of Code with Aymeric Fromherz and Nikos Gorogiannis: “Verification and Testing of Heap-based Programs with Symbolic PathFinder”.
2016—2017
(1 year)
Research Internship at IRIF (Université de Paris, France) with Ralf Treinen and Mihaela Sighireanu: “Correctness of Linux Scripts”.
2016
(6 months)
Research Internship at IRIF (Université de Paris, France) with Ralf Treinen and Mihaela Sighireanu: “Towards Verification of Shell Scripts”.
2015
(5 months)
Research Internship in the Complogic team (McGill University, Montréal, Canada) with Brigitte Pientka in order to help with the development of the proof assistant Beluga.
2014
(3 months)
Research Internship at the Institut de Mathématiques de Marseille (France) with Lionel Vaulx Auclair and Emmanuel Beffara: “On a logical counterpart of local non-determinism in classical realisability”.

Education

2013—2017
(4 years)
ENS Graduate Degree at the École normale supérieure (Paris, France). This is a research-oriented four-year program including the third year of bachelor, the two years of master and an extra year — in my case, a one year-long internship. The degree requires the validation of extra courses in addition to the bachelor and master.
2014—2016
(2 years)
Master's Degree in Computer Science at the Université de Paris (France). The “Master Parisien de Recherche en Informatique” is a research-oriented master program in computer science whose purpose is to train future scientists through intensive exposure to contemporary research.
2013—2014
(1 year)
Bachelor's Degree in Computer Science at the École normale supérieure (Paris, France). The two years of preparatory classes, completed by first year of the École normale supérieure, include a full bachelor.
2011—2013
(2 years)
Preparatory Classes MPSI/MP* at the Lycée du Parc (Lyon, France). Preparatory Classes are an intensive two-year preparation for competitive entrance into top engineering and research schools.

Miscellaneous Experience

2022—now President of the RSCDS Paris Branch. I lead the organising committee and represent the branch in front of the members, the RSCDS and the other branches.
2019—now Teacher of Scottish country dance classes at the RSCDS Paris Branch.
2018—now Musician for Scottish country dance classes at the RSCDS Paris Branch and internationally.
2019—2021 Editor of the Paris Book of Scottish Country Dances, volume 2 as well as its two companion books of tunes. This involves communicating with the different authors, handling copyright considerations, typesetting the book (using LaTeX and LilyPond), printing and publishing it, etc.
2018—2022 Member of the organising committee of the RSCDS Paris Branch.
2018—2022 Organiser and member of a professional band (~2-3 musicians) playing at various events, mostly weddings. This includes finding the gigs, discussing the organisation with the clients and, of course, playing music.
2017—2022 Organiser and member of an amateur band (~10-12 musicians) playing for Scottish country dances.
Jan. 2017 Student volunteer at POPL in Paris, France.
Aug. 2012 Sanitation worker for the city of Mions, France.
2009—2011 Member of the organising committee of the Orchestre d’Harmonie de Saint-Priest, an amateur wind orchestra, and its associated music school, Vive le Vent.

Selected Publications

2021 Verification of Shell Scripts Performing File Hierarchy Transformations”. Nicolas Jeannerod. PhD Thesis. PDF (not the final version). Dedicated Page.
2020 Analysing installation scenarios of Debian packages”. Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu and Ralf Treinen. In TACAS 2020 – 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Core Ranking 2020: A. Article.
2020 Morbig: A Static parser for POSIX shell”. Yann Régis-Gianas, Nicolas Jeannerod and Ralf Treinen. In Journal of Computer Languages, Volume 57, April 2020. Article.
2018 Morbig: A Static Parser for POSIX Shell”. Yann Régis-Gianas, Nicolas Jeannerod and Ralf Treinen. In SLE 2018 - 11th International Conference on Software Language Engineering. Core Ranking 2018: B. Article.
2018 Deciding the First-Order Theory of an Algebra of Feature Trees with Updates”. Nicolas Jeannerod and Ralf Treinen. In IJCAR 2018 - 9th International Joint Conference on Automated Reasoning. Core Ranking 2018: A*. Article. Extended Version.
2017 A Formally Verified Interpreter for a Shell-like Programming Language”. Nicolas Jeannerod, Claude Marché and Ralf Treinen. In VSTTE 2017 - 9th Working Conference on Verified Software: Theories, Tools and Experiments. Article.
2017 Le coquillage dans le CoLiS-mateur”. Nicolas Jeannerod. In JFLA 2017 - 28e Journées Francophones des Langages Applicatifs. Article. Archive.
See all my publications.

Selected Talks

Mar. 2021 Verification of Shell Scripts Performing File Hierarchy Transformations”. At PhD Thesis Defence.
Links: ⋅ Slides ⋅ Replay [MQ;LQ] ⋅ Dedicated Page ⋅ Thesis.
Dec. 2020 Analysing installation scenarios of Debian Packages”. At IRIF's Verification Seminar.
Links: ⋅ Slides ⋅ Demo ⋅ Replay ⋅ Associated article.
Sept. 2019 Symbolic Execution of Debian Packages”. At AVM'19.
Links: ⋅ Slides ⋅ Demo.
Jul. 2019 Symbolic Execution of Maintainer Scripts”. With Ralf Treinen. At DebConf'19.
Links: ⋅ Slides ⋅ Demo ⋅ Replay [LQ] .
Jul. 2018 Mining Debian Maintainer Scripts”. With Ralf Treinen. At DebConf'18.
Links: ⋅ Slides ⋅ Replay [LQ] .
Jul. 2018 Deciding the First-Order Theory of an Algebra of Feature Trees with Updates”. At IJCAR'18.
Links: ⋅ Slides ⋅ Associated article.
Jun. 2018 Deciding the First-Order Theory of an Algebra of Feature Trees with Updates”. At IRIF's Verification Seminar.
Links: ⋅ Slides ⋅ Associated article.
Sept. 2017 Formalising an Intermediate Language for POSIX Shell”. With Yann Régis-Gianas. At Seminar Gallium.
Links: ⋅ Slides.
Jul. 2017 A Formally Verified Interpreter for a Shell-like Programming Language”. At VSTTE'17.
Links: ⋅ Slides ⋅ Associated article.
Jul. 2017 A Formally Verified Interpreter for a Shell-like Programming Language”. At Seminar VALS.
Links: ⋅ Slides.
Jan. 2017 Le coquillage dans le CoLiS-mateur”. At JFLA'17.
Links: ⋅ Slides ⋅ Associated article.
See all my talks.

Teaching

Feb. 2020
(36h)
Internet et outils”. Practical exercises at Université de Paris (France): Introduction to web programming in HTML5/CSS/PHP/MySQL/JS for first year students in computing.
Sept. 2019
(24h)
Principe de fonctionnement des machines binaires”. Written exercises at Université de Paris (France): Introduction to binary, circuits and processors for first year students in computing.
Feb. 2019
(24h)
Concepts informatiques”. Written exercises at Université de Paris (France): Introduction to compilation for first year students in computing.
Sept. 2018
(36h)
Programmation fonctionnelle”. Practical exercises at Université de Paris (France): Introduction to functional programming in OCaml for third year students in computing.
Feb. 2018
(48h)
Internet et outils”. Practical exercises at Université de Paris (France): Introduction to web programming in HTML5/CSS/PHP/MySQL/JS for first year students in computing.
Feb. 2018
(24h)
Concepts informatiques”. Written exercises at Université de Paris (France): Introduction to compilation for first year students in computing.
Feb. 2017
(24h)
Projet informatique”. Tutoring at Université de Paris (France): tutoring of second year students in computing during their programming project.
Sept. 2016
(24h)
Introduction à la programmation”. Practical exercises at Université de Paris (France): Introduction to programming in Java for first year students in computing.