Research activities

Since October 2009:

I started my Phd thesis. I particularly focus on the combination of rewriting techniques in the SMT framework and the design of new decision procedures. My experiments are conducted in the Alt-Ergo theorem prover.

March - September 2009:

The core of the Alt-Ergo theorem prover relies on a Shostak-like congruence closure algorithm called CC(X). I extended this algorithm in order to integrate a built-in reasoning for user defined associative and commutative function symbols.

June - Augest 2008:

David Baudet and I participated to the Ocaml Summer Project funded by Jane Street Capital. During this project, we developped Ocamlwizard; a tool that provides a set of commandes for Ocaml IDEs.

March - May 2008:

I implemented a basic decision procedure for the theory of bit-vectors and integrated it in the Alt-Ergo theorem prover.

PS: Mohamed Iguernelala is NOT on Facebook, or Twitter, or LinkedIn, or Viadeo, or Tagged, . . . or any "social / professional network"