Vincent Nimal

Vincent Nimal

Doctoral Student

Leaving date: 14th May 2015

Themes:

Automated Verification

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	a static analyser synthesising memory fences for concurrent C program
	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.