Skip to main content

Vincent Nimal

Personal photo - Vincent Nimal

Vincent Nimal

Doctoral Student

Leaving date: 14th May 2015

Interests

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.

Tools

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

 

Biography

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.

Links

website fence website instrument
fence insertion weak memory instrumentation

Selected Publications

View AllManage publications

Supervisors