Welcome!

I have been an assistant professor at Grenoble INP – Ensimag since September 2007. I obtained my PhD in 2005 under the supervision of Thierry Boy de la Tour and Ricardo Caferra, and received a PhD award from INPG. I did postdoctoral research at the University of Verona (Italy) under the supervision of Maria Paola Bonacina before being recruited at Ensimag. I defended my Habilitation thesis (HDR) on Nov. 9th, 2017. The manuscript (in french) is available here.

I am mainly interested in automated reasoning, and have currently been working on:

  • Automated theorem provers for solving SMT problems
  • Finite instantiation methods
  • Inductive reasoning
  • Abductive reasoning
  • Separation logic

I have recently been interested in the formalization of financial mathematics using the proof assistant Isabelle. Some results about the formalization in Isabelle of the Cox-Ross-Rubinstein model can be found on this page.

Publications

Below is a (probably outdated) list of recent publications. A more complete list is available here.

Journal proceedings

  • Mnacho Echenim and Nicolas Peltier. A Superposition Calculus for Abductive Reasoning. Journal of Automated Reasoning, 2016. Paper
  • Vincent Aravantinos, Mnacho Echenim, and Nicolas Peltier. A resolution calculus for first-order schemata. Fundamenta Informaticae, 125(2):101133, 2013. Paper
  • Mnacho Echenim and Nicolas Peltier. Instantiation Schemes for Nested Theories. ACM Transactions on Computational Logic, 14(2):11, 2013. Paper
  • Mnacho Echenim and Nicolas Peltier. An instantiation scheme for satisfiability modulo theories. Journal of Automated Reasoning, 48(3), 2012. Paper

Conference and workshop proceedings

  • M. Echenim, N. Peltier, and S. Tourret. Quantifier-Free Equational Logic and Prime Implicate Generation. CADE 25,  2015. Paper
  • M. Echenim, N. Peltier, and S. Tourret. A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses. PAAR 2014. Paper
  • M. Echenim, N. Peltier, and S. Tourret. A Rewriting Strategy to Generate Prime Implicates in Equational Logic. IJCAR 2014. Paper
  • M. Echenim, N. Peltier, and S. Tourret. An approach to abductive reasoning in equational logic. IJCAI 2013. Extended version

 

Teaching

I have been co-head of the Financial Engineering department at Ensimag since 2009. These past years, I have been in charge of the following classes:

  • Formal Language Theory (Bac + 3). A possibly outdated version of the course notes (in french) is available here.
  • Logic bases for Computer Science (Bac + 4). The course notes (in french) are available here.
  • Introduction to the .NET platform (Bac + 5)

 

Contact Information

Office: LIG, Bâtiment IMAG. 700 avenue Centrale. 38401 St Martin d’Hères. FRANCE
Phone: +33 4 57 42 14 91
Email: Mnacho (dot) Echenim (at) univ-grenoble-alpes (dot) fr

Featuring WPMU Bloglist Widget by YD WordPress Developer