Skip to Main content
Number of documents

40

About


I am an assistant professor in Grenoble INP-Ensimag. I am a member of the CAPP group of the Grenoble Informatics Laboratory (LIG).


Journal articles10 documents

  • Mnacho Echenim, Radu Iosif, Nicolas Peltier. Entailment is Undecidable for Symbolic Heap Separation Logic Formulae with Non-Established Inductive Rules. Information Processing Letters, Elsevier, 2022. ⟨hal-02951859v2⟩
  • Mnacho Echenim, Hervé Guiol, Nicolas Peltier. Formalizing the Cox–Ross–Rubinstein Pricing of European Derivatives in Isabelle/HOL. Journal of Automated Reasoning, Springer Verlag, 2020, 64 (4), pp.737-765. ⟨10.1007/s10817-019-09528-w⟩. ⟨hal-02990376⟩
  • Mnacho Echenim, Radu Iosif, Nicolas Peltier. The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates. ACM Transactions on Computational Logic, Association for Computing Machinery, 2020. ⟨hal-02388326⟩
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. Prime Implicate Generation in Equational Logic. Journal of Artificial Intelligence Research, Association for the Advancement of Artificial Intelligence, 2017, 60, pp.827-880. ⟨hal-01946538⟩
  • Mnacho Echenim, Nicolas Peltier. A Superposition Calculus for Abductive Reasoning. Journal of Automated Reasoning, Springer Verlag, 2016, 57 (2), pp.97--134. ⟨hal-01363997⟩
  • Vincent Aravantinos, Mnacho Echenim, Nicolas Peltier. A Resolution Calculus for First-order Schemata. Fundamenta Informaticae, Polskie Towarzystwo Matematyczne, 2013, 125 (2), pp.101-133. ⟨10.3233/FI-2013-855⟩. ⟨hal-00933896⟩
  • Mnacho Echenim, Nicolas Peltier. Instantiation Schemes for Nested Theories. ACM Transactions on Computational Logic, Association for Computing Machinery, 2013, 14 (2), pp.11:1-33. ⟨10.1145/2480759.2480763⟩. ⟨hal-00933873⟩
  • Mnacho Echenim, Nicolas Peltier. An Instantiation Scheme for Satisfiability Modulo Theories. Journal of Automated Reasoning, Springer Verlag, 2012, 48 (3), pp.293-362. ⟨10.1007/s10817-010-9200-3⟩. ⟨hal-00933247⟩
  • Mnacho Echenim, Nicolas Peltier. Modular Instantiation Schemes. Information Processing Letters, Elsevier, 2011, 111 (20), pp.989-993. ⟨10.1016/j.ipl.2011.07.003⟩. ⟨hal-00931264⟩
  • Maria Paola Bonacina, Mnacho Echenim. Theory decision by decomposition. Journal of Symbolic Computation, Elsevier, 2010, 45 (2), pp.229-260. ⟨hal-00940845⟩

Conference papers19 documents

  • Mnacho Echenim, Radu Iosif, Nicolas Peltier. Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment. 29th EACSL Annual Conference on Computer Science Logic, Jan 2021, Ljubljana (virtual), Slovenia. ⟨10.4230/LIPIcs.CSL.2021.12⟩. ⟨hal-03040180⟩
  • Mnacho Echenim, Radu Iosif, Nicolas Peltier. Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment. 29th EACSL Annual Conference on Computer Science Logic, Jan 2021, Ljubljana, Slovenia. ⟨10.4230/LIPIcs.CSL.2021.12⟩. ⟨hal-03052687⟩
  • Mnacho Echenim, Radu Iosif, Nicolas Peltier. The Lower Bound of Decidable Entailments in Separation Logic with Inductive Definitions. ADSL 2020 - Workshop on Automated Deduction in Separation Logic, 2020, New Orleans, United States. ⟨hal-02388028⟩
  • Mnacho Echenim, Radu Iosif, Nicolas Peltier. Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard. LPAR 2020, 2020, Alicante, Spain. ⟨10.1145/3380809⟩. ⟨hal-02990396⟩
  • Mnacho Echenim, Radu Iosif, Nicolas Peltier. Prenex Separation Logic with One Selector Field. Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, 2019, London, United Kingdom. pp.409-427, ⟨10.1007/978-3-030-29026-9_23⟩. ⟨hal-02323468⟩
  • Mnacho Echenim, Radu Iosif, Nicolas Peltier. The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains. Foundations of Software Science and Computation Structures (FOSSACS) - 22nd International Conference, 2019, Prague, Czech Republic. pp.242-259, ⟨10.1007/978-3-030-17127-8_14⟩. ⟨hal-02094154⟩
  • Mnacho Echenim, Nicolas Peltier, Yanis Sellami. Ilinva: Using Abduction to Generate Loop Invariants. Frontiers of Combining Systems - 12th International Symposium, 2019, London, United Kingdom. pp.77-93, ⟨10.1007/978-3-030-29007-8_5⟩. ⟨hal-02323446⟩
  • Mnacho Echenim, Nicolas Peltier, Yanis Sellami. A Generic Framework for Implicate Generation Modulo Theories. IJCAR, Jul 2018, Oxford, United Kingdom. ⟨hal-01833514⟩
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. Prime Implicate Generation in Equational Logic. Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, 2018, Stockholm, Sweden. ⟨hal-01946497⟩
  • Nicolas Peltier, Mnacho Echenim. The Binomial Pricing Model in Finance: A Formalization in Isabelle. CADE 26, 2017, Gothenburg, Sweden. pp.546-562. ⟨hal-01562944⟩
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. Quantifier-Free Equational Logic and Prime Implicate Generation. CADE-25, Jul 2015, Berlin, Germany. pp.311-325, ⟨10.1007/978-3-319-21401-6_21⟩. ⟨hal-01363987⟩
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. A Superposition-Based Approach to Abductive Reasoning in Equational Clausal Logic. ADDTC 2014, Jul 2014, Vienna, Austria. ⟨hal-01132800⟩
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. A Rewriting Strategy to Generate Prime Implicates in Equational Logic. IJCAR 2014, Jul 2014, Vienna, Austria. pp.137-151. ⟨hal-01018692⟩
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses. PAAR 2014, Jul 2014, Vienna, Austria. ⟨hal-01132801⟩
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. An Approach to Abductive Reasoning in Equational Logic. IJCAI 2013 - International Joint Conference on Artificial Intelligence, Aug 2013, Beijing, China. pp.531-537. ⟨hal-00934278⟩
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. A Superposition Strategy for Abductive Reasoning in Ground Equational Logic. IWS 2012 - International Workshop on Strategies in Rewriting, Proving and Programming (IJCAR 2012 workshop ), Jul 2012, Manchester, United Kingdom. pp.4-11. ⟨hal-00933582⟩
  • Mnacho Echenim, Nicolas Peltier. A Calculus for Generating Ground Explanations. IJCAR 2012 - International Joint Conference on Automated Reasoning, Jun 2012, Manchester, United Kingdom. pp.194-209, ⟨10.1007/978-3-642-31365-3_17⟩. ⟨hal-00933272⟩
  • Mnacho Echenim, Nicolas Peltier. Reasoning on Schemata of Formulæ. AISC 2012 - Artificial Intelligence and Symbolic Computation (Part of CICM 2012), Jul 2012, Bremen, Germany. pp.310-325, ⟨10.1007/978-3-642-31374-5_21⟩. ⟨hal-00933516⟩
  • Mnacho Echenim, Nicolas Peltier. Instantiation of SMT Problems Modulo Integers. International Conference on Artificial Intelligence and Symbolic Computation, 2010, Paris, France. pp.49-63, ⟨10.1007/978-3-642-14128-7_6⟩. ⟨hal-00940668⟩

Other publications1 document

Preprints, Working Papers, ...5 documents

  • Mnacho Echenim, Herve Guiol, Nicolas Peltier. Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL. 2018. ⟨hal-01954948⟩
  • Mnacho Echenim, Radu Iosif, Nicolas Peltier. On the Expressive Completeness of Bernays-Sch\"onfinkel-Ramsey Separation Logic. 2018. ⟨hal-01699151⟩
  • Mnacho Echenim, Radu Iosif, Nicolas Peltier. The Complexity of Prenex Separation Logic with One Selector. 2018. ⟨hal-01946528⟩
  • Thierry Boy de la Tour, Mnacho Echenim. Solving Linear Constraints in Elementary Abelian p-Groups of Symmetries. 2011. ⟨hal-00940852⟩
  • Mnacho Echenim, Nicolas Peltier. Instantiation of SMT problems modulo Integers. 2010. ⟨hal-00940677⟩

Reports4 documents

  • Nicolas Peltier, Radu Iosif, Mnacho Echenim. Checking Entailment Between Separation Logic Symbolic Heaps: Beyond Connected and Established Systems. [Research Report] VERIMAG/LIG/CNRS. 2020. ⟨hal-03088890⟩
  • Mnacho Echenim, Nicolas Peltier. A Calculus for Generating Ground Explanations (Technical Report). 2012. ⟨hal-00933750⟩
  • Vincent Aravantinos, Mnacho Echenim, Nicolas Peltier. A Resolution Calculus for Propositional Schemata. 2011. ⟨hal-00932855⟩
  • Vincent Aravantinos, Mnacho Echenim, Nicolas Peltier. A Resolution Calculus for First-Order Schemata. 2011. ⟨hal-00932856⟩

Theses1 document

  • Mnacho Echenim. Déduction et Unification dans les Théories Permutatives. Autre [cs.OH]. Institut National Polytechnique de Grenoble - INPG, 2005. Français. ⟨tel-00011236⟩