During daytime, I work for Tarides on the OCaml language, which is a high-level language, both safe and performant, that I like a lot. I generally work on free or open source software, so you can consult my current activity on my Github profile.
Part of the rest of my time is spent reading philosophy or various novels (with an inclination toward SF), or hacking on a typesetting software.
Before my current job, I did a PhD at CEA List and ENS under the supervision of Matthieu Lemerre and Xavier Rival. I worked on static analysis of low-level code in order to verify the security of kernel (among other things).
I'm also interested in functional programming, type systems and logic.
My name is pronounced ɔ.li'vje ni'kol, but “Oliver” with the usual English pronunciation is also fine.
- I have contributed to implement mathematics typesetting into the SILE typesetter.
- haskell-chess: a ridiculously simple and incomplete chess engine in Haskell. May be completed some day.
- spino: an attempt to encode the logical structure of Spinoza’s “Ethics” in the proof language Agda. The work is based on Jarrett, The logical structure of Spinoza's Ethics, Part I.
- Multicoretests – Parallel Testing Libraries for OCaml 5.0 (extended abstract)
Jan Midtgaard, Olivier Nicole and Nicolas Osborne
OCaml Workshop 2022
Automatically Proving Microkernel Security
video in French)
RESSI 2020 (Rendez-vous de la Recherche et de l'Enseignement de la Sécurité des Systèmes d'Information), short paper
Modular Macros (Poster/Demo Talk) (pdf)
Olivier Nicole, Leo White and Jeremy Yallop
Lightweight Shape Analysis based on Physical Types
Olivier Nicole, Matthieu Lemerre, Xavier Rival
VMCAI 2022 (Verification, Model Checking and Abstract Interpretation)
No Crash, No Exploit: Automated Verification of Embedded Kernels
Olivier Nicole, Matthieu Lemerre, Sébastien Bardin, Xavier Rival
RTAS 2021 (IEEE Real-Time and Embedded Technology and Applications Symposium)
Best Paper Award
Automated Verification of Systems Code using Type-based Memory Abstractions
- PDF for screens, for printing (hyperlinks not colored)
- Video of the defense (in English)
- Mathematics S1: Elementary logic. L1 level, CRI Paris (12 h)
- Mathematics S2: Linear algebra. L1 level, CRI Paris (12 h)
- Éléments de programmation (Elements of Programming) — LU1IN001. L1 level, Sorbonne Université (19 h)
- Programmation en C (C Programming) — PRC05. L3 level, École d'ingénieurs Denis Diderot, Université Paris 7 (27 h)
- Systèmes d'exploitations (Operating Systems) — IN201. M1 level, ENSTA Paris (15 h)