Mnacho Echenim

74 papers A* 2A 9B 6C 1Journal 46Unranked 9

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Concentrated Liquidity Market Making Operations. Arch. Formal Proofs Mnacho Echenim
2026	J	`jnl`	Uniswap V3: Impermanent Loss Modeling and Swap Fees Asymptotic Analysis. SIAM J. Financial Math. Mnacho Echenim, Emmanuel Gobet, Anne-Claire Maurice
2025	J	`jnl`	A Direct Procedure to Test Entailment in a Separation Logic of Relations. J. Autom. Reason. Mnacho Echenim, Nicolas Peltier
2025	J	`jnl`	Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates. Fundam. Informaticae Mnacho Echenim, Nicolas Peltier
2024	J	`jnl`	A Formalization of the CHSH Inequality and Tsirelson's Upper-bound in Isabelle/HOL. J. Autom. Reason. Mnacho Echenim, Mehdi Mhalla
2023	J	`jnl`	A Proof Procedure for Separation Logic with Inductive Definitions and Data. J. Autom. Reason. Mnacho Echenim, Nicolas Peltier
2023	B	`conf`	A Strict Constrained Superposition Calculus for Graphs. FoSSaCS Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier
2023	J	`jnl`	A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL. CoRR Mnacho Echenim, Mehdi Mhalla
2023	J	`jnl`	An undecidability result for Separation Logic with theory reasoning. Inf. Process. Lett. Mnacho Echenim, Nicolas Peltier
2023	J	`jnl`	The CHSH inequality: Tsirelson's upper-bound and other results. Arch. Formal Proofs Mnacho Echenim, Mehdi Mhalla, Coraline Mori
2023	J	`jnl`	Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates. CoRR Mnacho Echenim, Nicolas Peltier
2022	J	`jnl`	A Proof Procedure For Separation Logic With Inductive Definitions and Theory Reasoning. CoRR Mnacho Echenim, Nicolas Peltier
2022	J	`jnl`	Entailment is Undecidable for Symbolic Heap Separation Logic Formulæ with Non-Established Inductive Rules. Inf. Process. Lett. Mnacho Echenim, Radu Iosif, Nicolas Peltier
2022	J	`jnl`	Simultaneous diagonalization of pairwise commuting Hermitian matrices. Arch. Formal Proofs Mnacho Echenim
2022	J	`jnl`	Two Results on Separation Logic With Theory Reasoning. CoRR Mnacho Echenim, Nicolas Peltier
2021	C	`conf`	A Superposition-Based Calculus for Diagrammatic Reasoning. PPDP Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier
2021	J	`jnl`	A Superposition-Based Calculus for Quantum Diagrammatic Reasoning and Beyond. CoRR Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier
2021	B	`conf`	Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment. CSL Mnacho Echenim, Radu Iosif, Nicolas Peltier
2021	J	`jnl`	Quantum projective measurements and the CHSH inequality in Isabelle/HOL. CoRR Mnacho Echenim, Mehdi Mhalla
2021	J	`jnl`	Quantum projective measurements and the CHSH inequality. Arch. Formal Proofs Mnacho Echenim
2021	J	`jnl`	The Hahn and Jordan Decomposition Theorems. Arch. Formal Proofs Marie Cousin, Mnacho Echenim, Hervé Guiol
2021	A	`conf`	Unifying Decidable Entailments in Separation Logic with Inductive Definitions. CADE Mnacho Echenim, Radu Iosif, Nicolas Peltier
2020	J	`jnl`	Checking Entailment Between Separation Logic Symbolic Heaps: Beyond Connected and Established Systems. CoRR Mnacho Echenim, Radu Iosif, Nicolas Peltier
2020	J	`jnl`	Combining Induction and Saturation-Based Theorem Proving. J. Autom. Reason. Mnacho Echenim, Nicolas Peltier
2020	J	`jnl`	Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Established Systems. CoRR Mnacho Echenim, Radu Iosif, Nicolas Peltier
2020	B	`conf`	Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard. LPAR Mnacho Echenim, Radu Iosif, Nicolas Peltier
2020	J	`jnl`	Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard. CoRR Mnacho Echenim, Radu Iosif, Nicolas Peltier
2020	J	`jnl`	Formalizing the Cox-Ross-Rubinstein Pricing of European Derivatives in Isabelle/HOL. J. Autom. Reason. Mnacho Echenim, Hervé Guiol, Nicolas Peltier
2020	J	`jnl`	The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates. ACM Trans. Comput. Log. Mnacho Echenim, Radu Iosif, Nicolas Peltier
2019	—	`conf`	Ilinva: Using Abduction to Generate Loop Invariants. FroCos Mnacho Echenim, Nicolas Peltier, Yanis Sellami
2019	J	`jnl`	Ilinva: Using Abduction to Generate Loop Invariants. CoRR Mnacho Echenim, Nicolas Peltier, Yanis Sellami
2019	B	`conf`	Prenex Separation Logic with One Selector Field. TABLEAUX Mnacho Echenim, Radu Iosif, Nicolas Peltier
2019	B	`conf`	The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains. FoSSaCS Mnacho Echenim, Radu Iosif, Nicolas Peltier
2018	A	`conf`	A Generic Framework for Implicate Generation Modulo Theories. IJCAR Mnacho Echenim, Nicolas Peltier, Yanis Sellami
2018	J	`jnl`	A Generic Framework for Implicate Generation Modulo Theories. CoRR Mnacho Echenim, Nicolas Peltier, Yanis Sellami
2018	J	`jnl`	Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL. CoRR Mnacho Echenim, Hervé Guiol, Nicolas Peltier
2018	J	`jnl`	On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic. CoRR Mnacho Echenim, Radu Iosif, Nicolas Peltier
2018	J	`jnl`	Pricing in discrete financial models. Arch. Formal Proofs Mnacho Echenim
2018	A*	`conf`	Prime Implicate Generation in Equational Logic (extended abstract). IJCAI Mnacho Echenim, Nicolas Peltier, Sophie Tourret
2018	J	`jnl`	The Complexity of Prenex Separation Logic with One Selector. CoRR Mnacho Echenim, Radu Iosif, Nicolas Peltier
2017	J	`jnl`	Prime Implicate Generation in Equational Logic. J. Artif. Intell. Res. Mnacho Echenim, Nicolas Peltier, Sophie Tourret
2017	A	`conf`	The Binomial Pricing Model in Finance: A Formalization in Isabelle. CADE Mnacho Echenim, Nicolas Peltier
2016	J	`jnl`	A Superposition Calculus for Abductive Reasoning. J. Autom. Reason. Mnacho Echenim, Nicolas Peltier
2015	A	`conf`	Quantifier-Free Equational Logic and Prime Implicate Generation. CADE Mnacho Echenim, Nicolas Peltier, Sophie Tourret
2014	—	`conf`	A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses. PAAR@IJCAR Sophie Tourret, Mnacho Echenim, Nicolas Peltier
2014	A	`conf`	A Rewriting Strategy to Generate Prime Implicates in Equational Logic. IJCAR Mnacho Echenim, Nicolas Peltier, Sophie Tourret
2014	J	`jnl`	A Superposition Calculus for Abductive Reasoning. CoRR Mnacho Echenim, Nicolas Peltier
2013	J	`jnl`	A Resolution Calculus for First-order Schemata. Fundam. Informaticae Vincent Aravantinos, Mnacho Echenim, Nicolas Peltier
2013	A*	`conf`	An Approach to Abductive Reasoning in Equational Logic. IJCAI Mnacho Echenim, Nicolas Peltier, Sophie Tourret
2013	J	`jnl`	Instantiation Schemes for Nested Theories. ACM Trans. Comput. Log. Mnacho Echenim, Nicolas Peltier
2012	J	`jnl`	A Calculus for Generating Ground Explanations (Technical Report) CoRR Mnacho Echenim, Nicolas Peltier
2012	A	`conf`	A Calculus for Generating Ground Explanations. IJCAR Mnacho Echenim, Nicolas Peltier
2012	J	`jnl`	An Instantiation Scheme for Satisfiability Modulo Theories. J. Autom. Reason. Mnacho Echenim, Nicolas Peltier
2012	J	`jnl`	Reasoning on Schemata of Formulae CoRR Mnacho Echenim, Nicolas Peltier
2012	—	`conf`	Reasoning on Schemata of Formulæ. AISC/MKM/Calculemus Mnacho Echenim, Nicolas Peltier
2011	J	`jnl`	Instantiation Schemes for Nested Theories CoRR Mnacho Echenim, Nicolas Peltier
2011	J	`jnl`	Modular instantiation schemes. Inf. Process. Lett. Mnacho Echenim, Nicolas Peltier
2011	J	`jnl`	Solving Linear Constraints in Elementary Abelian p-Groups of Symmetries CoRR Thierry Boy de la Tour, Mnacho Echenim
2010	—	`conf`	Instantiation of SMT Problems Modulo Integers. AISC/MKM/Calculemus Mnacho Echenim, Nicolas Peltier
2010	J	`jnl`	Instantiation of SMT problems modulo Integers CoRR Mnacho Echenim, Nicolas Peltier
2010	J	`jnl`	Theory decision by decomposition. J. Symb. Comput. Maria Paola Bonacina, Mnacho Echenim
2008	J	`jnl`	On Variable-inactivity and Polynomial tau-Satisfiability Procedures. J. Log. Comput. Maria Paola Bonacina, Mnacho Echenim
2008	A	`conf`	Unification and Matching Modulo Leaf-Permutative Equational Presentations. IJCAR Thierry Boy de la Tour, Mnacho Echenim, Paliath Narendran
2007	—	`conf`	Determining Unify-Stable Presentations. RTA Thierry Boy de la Tour, Mnacho Echenim
2007	J	`jnl`	Permutative rewriting and unification. Inf. Comput. Thierry Boy de la Tour, Mnacho Echenim
2007	A	`conf`	T-Decision by Decomposition. CADE Maria Paola Bonacina, Mnacho Echenim
2006	—	`conf`	Rewrite-Based Decision Procedures. STRATEGIES@IJCAR Maria Paola Bonacina, Mnacho Echenim
2006	—	`conf`	Rewrite-Based Satisfiability Procedures for Recursive Data Structures. PDPAR/PaUL@FLoC Maria Paola Bonacina, Mnacho Echenim
2005	—	`—`	Déduction et Unification dans les Théories Permutatives. (Deduction and Unification in Permutative Theories). Mnacho Echenim
2005	—	`conf`	Unification in a Class of Permutative Theories. RTA Thierry Boy de la Tour, Mnacho Echenim
2004	J	`jnl`	On the Complexity of Deduction Modulo Leaf Permutative Equations. J. Autom. Reason. Thierry Boy de la Tour, Mnacho Echenim
2004	A	`conf`	Overlapping Leaf Permutative Equations. IJCAR Thierry Boy de la Tour, Mnacho Echenim
2003	B	`conf`	NP-Completeness Results for Deductive Problems on Stratified Terms. LPAR Thierry Boy de la Tour, Mnacho Echenim
2003	—	`conf`	On Leaf Permutative Theories and Occurrence Permutation Groups. FTP Thierry Boy de la Tour, Mnacho Echenim