Skip to main content

Vincent Nimal

Personal photo - Vincent Nimal

Vincent Nimal

Doctoral Student

Leaving date: 14th May 2015


I work on applications of static analyses to weak memory models, with a specific interest in scalability issues in practice. In particular, I developed the weak memory program transformation in goto-instrument (distributed with the model checker CBMC) and the automatic memory fence synthesiser musketeer. During my Master thesis, I also worked on statistical approaches to probabilistic model checking. This work has been integrated into the probabilistic model checker Prism.


musketeer image musketeer a static analyser synthesising memory fences for concurrent C program
bowtie image goto-instrument --mm a source-to-source transformer for concurrent C program that makes weak memory reorderings visible to sequentially consistent tools



I joined Daniel Kroening's group in 2010 after having completed an MSc in Computer Science in Oxford (with distinction). I interned at Microsoft Research India during summer 2012, working on improving the exploration strategy in the model checker Corral. I also hold a French Engineering Degree (~MSc) in applied mathematics and computer science from ENSIIE Paris-Evry, and did two internships at CEA (Atomic Energy Commission) and MLstate, Paris during my undergraduate studies.


website fence website instrument
fence insertion weak memory instrumentation

Selected Publications

View AllManage publications