Nicolas “Niols” Jeannerod

Top

Curriculum Vitæ

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

Career

2017—2021
(3½ years)
Ph.D. 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”.
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, or about my education.

Ph.D. Thesis

Goal Applying formal techniques to Shell scripts in order to find bugs in Debian packages.
Logics Researching on the decidability of feature tree logics, with efficiency considerations and implementation of satisfiability solvers.
Implem. Writing tools to parse, transform and analyse Shell scripts and Debian packages. This comprises reading standard, modeling various real-world objects and implementing. The tools had to be able to scale to thousands of packages.
Bugs Reported 152 bugs, 109 of which have been fixed.
See more about my Ph.D. 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 PHP/SQL/HTML/CSS, TeX/LaTeX OK C, Java, Python, JavaScript, 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 Member of the organising committee of CONFLANG, a workshop colocated with SPLASH in October 2021.
2017—2021
(3½ years)
Ph.D. 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”.
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

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.
2019—now Teacher of Scottish country dance classes at the RSCDS Paris Branch.
2018—2022 Member of the organising committee of the RSCDS Paris Branch.
2018—now 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.
2018—now Musician for Scottish country dance classes at the RSCDS Paris Branch.
2017—now 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. Ph.D. 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 Ph.D. 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.