(You can also get this curriculum vitæ as PDF.)
| 2021—now | Research Software Engineer at Tweag I/O. I spent a year working for a client and building a dynamic analysis tool suite for smart contracts on Cardano, mostly in Racket. I then joined the internal High Assurance Software Group a year ago, where I worked towards a similar purpose on a different tool suite written in Haskell. I am now working for a client and implementing an improvement of a consensus algorithm. In parallel, I contribute to some internal projects. I am also a hive supporter, mentoring fellow engineers as well as following them and communicating on their behalf to other instances of the company. |
| 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. |
| 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. |
| Main | OCaml, POSIX Shell | Natural | Fluent in French and English |
| Good | Haskell, Racket, TeX/LaTeX | OK | Web, C, Java, Python, other Lisp |
| 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. |
| 2021—now | Research Software Engineer at Tweag I/O. I spent a year working for a client and building a dynamic analysis tool suite for smart contracts on Cardano, mostly in Racket. I then joined the internal High Assurance Software Group a year ago, where I worked towards a similar purpose on a different tool suite written in Haskell. I am now working for a client and implementing an improvement of a consensus algorithm. In parallel, I contribute to some internal projects. I am also a hive supporter, mentoring fellow engineers as well as following them and communicating on their behalf to other instances of the company. |
| 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”. |
| 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. |
| 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. |
| 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. |
| 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. |
| 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. |