Presentation
Hi, I am Vincent Rébiscoul and my website is still in
construction. I will try to update it as soon as possible. I
used to be a computer science master student
at École Normale Supérieure
de Lyon, and I am currently a PhD student at INRIA in the Epicure team.
I am interested in proof of programs, static code
analysis, formal verification and compilation.
I am currently working on building static analyses from Skeletal Semantics.
A skeletal semantics is a description of a language. This description is written in Skel, a small functional language.
If you want to
contact me, encrypt your mail using
my public key.
Skills
Languages
- French, native
- English, C1 CEFR level. I passed the Cambridge Advanced Exam.
Programming languages
I know C and OCaml well. I also know Python, C++, HTML, and Java.Background
CPGE (2014-2016), Lycée Berthollet, Annecy
Two years of intensive preparation to competitive exams for "Grandes Écoles". There, I mainly studied mathematics, physics and computer science.
BsC in Computer Science (2016-2017), École Normale Supérieure de Lyon
MsC in Computer Science (2017-2019), École Normale Supérieure de Lyon
I obtained my master of Fundamental Computer Science in June 2019.
Projet Long de Recherche "PLR" (2019-2020)
A PLR is a year during which the student does two or three research internships which are less supervised than the previous internships. It allows the student to discover new fields or to precise what he wants to do during a PhD.
Experience
Research Internship of 6 weeks (May 2017 - July 2017), INRIA Grenoble, POLARIS team
I spent 6 weeks working on the subject Optimisation avec incertitudes: application à la gestion énergétique, under the supervision of Bruno Gaujal. I studied Markov Decision Processes and I implemented an algorithm which purpose was to solve a Bellman's equation using dynamic programming. You can find my report here and the code of my algorithm is on Github.
Research Internship of 11 weeks (May 2018, July 2018), Chalmers University of Techology, Formal Methods group
For 11 weeks I worked on the verification of Solidity Smart Contracts under the supervision of Wolfgang Ahrendt. The goal was to translate Solidity Smart Contracts into Java programs to then use the KeY prover to prove some properties on the Solidity program. I coded a program Javadity to perform the translation from Solidity to Java automatically.
Research Internship of 4.5 months (February 2019, June 2019), INRIA Paris, ANTIQUE team
During this internship in the Antique team under the supervision of Xavier Rival, we created an extension of Separation Logic to describe non-inductive data structures. We then created an abstract domain that we implemented in the MemCAD shape analyzer.
Research Internship of 5 months (October 2019, February 2019), INRIA Rennes, CELTIQUE team
During this internship I will work on Skeletal Semantics. The goal is to perform a Control Flow Analysis (0-CFA) using skeletal semantics which will generate constraints. Once the constraints are solved (using an already existing tool), it will give a solution of the CFA and this solution will need to be checked in Coq.