I started my Phd thesis. It aims at combining powerfull forward proof search techniques and backward methods.

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.

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.

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

Sylvain Conchon, Evelyne Contejean, and Mohamed Iguernelala. Ground Associative and Commutative Completion Modulo Shostak Theories. In Logic for Programming, Articifial Intelligence and Reasoning (LPAR 17), Yogyakarta, Indonesia, 2010. Easychair Volume. Short paper. [pdf]

Sylvain Conchon, Evelyne Contejean, and Mohamed Iguernelala. Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. Research Report 1538, LRI, Paris-Sud University, December 2010. [pdf]

Sylvain Conchon, Evelyne Contejean, and Mohamed Iguernelala. Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 17), Saarbrücken, Germany, 2011. [Best theoretical paper at ETAPS 2011]