SMTCoq | Communication between Coq and SAT/SMT solvers
Presentation | Louise Dubois de Prisque
Welcome to my former research page (do not hesitate to contact me if you have a question about one of my articles). I moved to the industry in october 2022 and am currently looking for a position as a software engineer and/or anything that involves (non-elementary) maths! You may find my resume here and my LinkedIn profile there . This page should welcome soon some other material beyond computer science :)
The last academic position I occupied was a post-doc in the Deducteam in the LMF (Laboratoire Méthodes Formelles), located in ENS Paris-Saclay (south of Paris), under the supervision of Chantal Keller and Valentin Blot . There, I was part of the development team of the Coq module Sniper , which help do some proof automation in Coq. I used to be a Phd student at IRIF (Paris) and a post-doc in the Gallinette Inria team (Nantes).
The first release of Sniper is out! An involved version of the motivation and the techniques behind Sniper can be found here as a preprint (with V. Blot , D. Cousineau, Enzo Crance, L. Dubois de Prisque, C. Keller , A. Mahboubi) .
SMTCoq | Communication between Coq and SAT/SMT solvers
Presentation | Louise Dubois de Prisque