| 2023 | FOSSACS | A Strict Constrained Superposition Calculus for Graphs. | Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier |
| 2021 | CADE | Unifying Decidable Entailments in Separation Logic with Inductive Definitions. | Mnacho Echenim, Radu Iosif, Nicolas Peltier |
| 2021 | CSL | Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment. | Mnacho Echenim, Radu Iosif, Nicolas Peltier |
| 2021 | PPDP | A Superposition-Based Calculus for Diagrammatic Reasoning. | Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier |
| 2020 | LPAR | Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard. | Mnacho Echenim, Radu Iosif, Nicolas Peltier |
| 2019 | FOSSACS | The Bernays-Schnfinkel-Ramsey Class of Separation Logic on Arbitrary Domains. | Mnacho Echenim, Radu Iosif, Nicolas Peltier |
| 2019 | TABLEAUX | Prenex Separation Logic with One Selector Field. | Mnacho Echenim, Radu Iosif, Nicolas Peltier |
| 2018 | CADE | A Generic Framework for Implicate Generation Modulo Theories. | Mnacho Echenim, Nicolas Peltier, Yanis Sellami |
| 2018 | IJCAI | Prime Implicate Generation in Equational Logic (extended abstract). | Mnacho Echenim, Nicolas Peltier, Sophie Tourret |
| 2017 | CADE | The Binomial Pricing Model in Finance: A Formalization in Isabelle. | Mnacho Echenim, Nicolas Peltier |
| 2015 | CADE | Quantifier-Free Equational Logic and Prime Implicate Generation. | Mnacho Echenim, Nicolas Peltier, Sophie Tourret |
| 2014 | CADE | A Rewriting Strategy to Generate Prime Implicates in Equational Logic. | Mnacho Echenim, Nicolas Peltier, Sophie Tourret |
| 2014 | CADE | A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses. | Sophie Tourret, Mnacho Echenim, Nicolas Peltier |
| 2013 | IJCAI | An Approach to Abductive Reasoning in Equational Logic. | Mnacho Echenim, Nicolas Peltier, Sophie Tourret |
| 2012 | AISC | Reasoning on Schemata of Formul. | Mnacho Echenim, Nicolas Peltier |
| 2012 | CADE | A Calculus for Generating Ground Explanations. | Mnacho Echenim, Nicolas Peltier |
| 2010 | AISC | Instantiation of SMT Problems Modulo Integers. | Mnacho Echenim, Nicolas Peltier |
| 2008 | CADE | Unification and Matching Modulo Leaf-Permutative Equational Presentations. | Thierry Boy de la Tour, Mnacho Echenim, Paliath Narendran |
| 2007 | CADE | T-Decision by Decomposition. | Maria Paola Bonacina, Mnacho Echenim |
| 2004 | CADE | Overlapping Leaf Permutative Equations. | Thierry Boy de la Tour, Mnacho Echenim |
| 2003 | LPAR | NP-Completeness Results for Deductive Problems on Stratified Terms. | Thierry Boy de la Tour, Mnacho Echenim |