Nicolas Peltier

ORCID

Publication Activity (10 Years)

Years Active: 1994-2024
Publications (10 Years): 45

Top Venues

Grenoble Institute of Technology, France (PHD)

Education History

Grenoble Institute of Technology, France

PHD

Publications

Tanguy Bozec, Nicolas Peltier, Quentin Petitjean, Mihaela Sighireanu
What Is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment? IJCAR (2) (2024)
Nicolas Peltier
An EXPTIME-Complete Entailment Problem in Separation Logic. WoLLIC (2024)
Nicolas Peltier
Some techniques for reasoning automatically on co-inductive data structures. J. Log. Comput. 34 (3) (2024)
Nicolas Peltier
Testing the Satisfiability of Formulas in Separation Logic with Permissions. TABLEAUX (2023)
Mnacho Echenim, Nicolas Peltier
A Proof Procedure for Separation Logic with Inductive Definitions and Data. J. Autom. Reason. 67 (3) (2023)
Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier
A Strict Constrained Superposition Calculus for Graphs. FoSSaCS (2023)
Mnacho Echenim, Nicolas Peltier
An undecidability result for Separation Logic with theory reasoning. Inf. Process. Lett. 182 (2023)
Mnacho Echenim, Nicolas Peltier
Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates. CoRR (2023)
Mnacho Echenim, Nicolas Peltier
A Proof Procedure For Separation Logic With Inductive Definitions and Theory Reasoning. CoRR (2022)
Nicolas Peltier, Viorica Sofronie-Stokkermans
Special Issue of Selected Extended Papers of IJCAR 2020. J. Autom. Reason. 66 (3) (2022)
Nicolas Peltier
Reasoning on Dynamic Transformations of Symbolic Heaps. TIME (2022)
Mnacho Echenim, Nicolas Peltier
Two Results on Separation Logic With Theory Reasoning. CoRR (2022)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
Entailment is Undecidable for Symbolic Heap Separation Logic Formulæ with Non-Established Inductive Rules. Inf. Process. Lett. 173 (2022)
Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier
A Superposition-Based Calculus for Diagrammatic Reasoning. PPDP (2021)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment. CSL (2021)
Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier
A Superposition-Based Calculus for Quantum Diagrammatic Reasoning and Beyond. CoRR (2021)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
Unifying Decidable Entailments in Separation Logic with Inductive Definitions. CADE (2021)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard. CoRR (2020)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
Checking Entailment Between Separation Logic Symbolic Heaps: Beyond Connected and Established Systems. CoRR (2020)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Established Systems. CoRR (2020)
Mnacho Echenim, Nicolas Peltier
Combining Induction and Saturation-Based Theorem Proving. J. Autom. Reason. 64 (2) (2020)
Mnacho Echenim, Hervé Guiol, Nicolas Peltier
Formalizing the Cox-Ross-Rubinstein Pricing of European Derivatives in Isabelle/HOL. J. Autom. Reason. 64 (4) (2020)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard. LPAR (2020)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates. ACM Trans. Comput. Log. 21 (3) (2020)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
Prenex Separation Logic with One Selector Field. TABLEAUX (2019)
Mnacho Echenim, Nicolas Peltier, Yanis Sellami
Ilinva: Using Abduction to Generate Loop Invariants. FroCos (2019)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains. FoSSaCS (2019)
Mnacho Echenim, Nicolas Peltier, Yanis Sellami
Ilinva: Using Abduction to Generate Loop Invariants. CoRR (2019)
Mnacho Echenim, Hervé Guiol, Nicolas Peltier
Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL. CoRR (2018)
Michael Peter Lettmann, Nicolas Peltier
A Tableaux Calculus for Reducing Proof Size. CoRR (2018)
Mnacho Echenim, Nicolas Peltier, Yanis Sellami
A Generic Framework for Implicate Generation Modulo Theories. CoRR (2018)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic. CoRR (2018)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
The Complexity of Prenex Separation Logic with One Selector. CoRR (2018)
Mnacho Echenim, Nicolas Peltier, Yanis Sellami
A Generic Framework for Implicate Generation Modulo Theories. IJCAR (2018)
Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard
Superposition with Datatypes and Codatatypes. IJCAR (2018)
Michael Peter Lettmann, Nicolas Peltier
A Tableaux Calculus for Reducing Proof Size. IJCAR (2018)
Mnacho Echenim, Nicolas Peltier, Sophie Tourret
Prime Implicate Generation in Equational Logic (extended abstract). IJCAI (2018)
Mnacho Echenim, Nicolas Peltier, Sophie Tourret
Prime Implicate Generation in Equational Logic. J. Artif. Intell. Res. 60 (2017)
Nicolas Peltier
A paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules. J. Log. Comput. 27 (2) (2017)
Mnacho Echenim, Nicolas Peltier
The Binomial Pricing Model in Finance: A Formalization in Isabelle. CADE (2017)
Alexander Leitsch, Nicolas Peltier, Daniel Weller
CERES for first-order schemata. J. Log. Comput. 27 (7) (2017)
Nicolas Peltier
A Variant of the Superposition Calculus. Arch. Formal Proofs 2016 (2016)
Thierry Boy de la Tour, Nicolas Peltier
Proof Generalization in $$\mathrm {LK}$$ LK by Second Order Unifier Minimization. J. Autom. Reason. 57 (3) (2016)
Nicolas Peltier
Propositional Resolution and Prime Implicates Generation. Arch. Formal Proofs 2016 (2016)
Mnacho Echenim, Nicolas Peltier
A Superposition Calculus for Abductive Reasoning. J. Autom. Reason. 57 (2) (2016)
Mnacho Echenim, Nicolas Peltier, Sophie Tourret
Quantifier-Free Equational Logic and Prime Implicate Generation. CADE (2015)
Tanguy Sassolas, Chiara Sandionigi, Alexandre Guerre, Julien Mottin, Pascal Vivet, Hela Boussetta, Nicolas Peltier
A simulation framework for rapid prototyping and evaluation of thermal mitigation techniques in many-core architectures. ISLPED (2015)
Nicolas Peltier
Reasoning on Schemas of Formulas: An Automata-Based Approach. LATA (2015)
Tanguy Sassolas, Chiara Sandionigi, Alexandre Guerre, Alexandre Aminot, Pascal Vivet, Hela Boussetta, Luca Ferro, Nicolas Peltier
Early design stage thermal evaluation and mitigation: The locomotiv architectural case. DATE (2014)
Cristiano Santos, Pascal Vivet, Gene Matter, Nicolas Peltier, Sylvian Kaiser, Ricardo Augusto da Luz Reis
Thermal modeling methodology for efficient system-level thermal analysis. CICC (2014)
Nicolas Peltier
Tractable and intractable classes of propositional schemata. J. Log. Comput. 24 (5) (2014)
Mnacho Echenim, Nicolas Peltier, Sophie Tourret
A Rewriting Strategy to Generate Prime Implicates in Equational Logic. IJCAR (2014)
Mnacho Echenim, Nicolas Peltier
A Superposition Calculus for Abductive Reasoning. CoRR (2014)
Sophie Tourret, Mnacho Echenim, Nicolas Peltier
A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses. PAAR@IJCAR (2014)
Hicham Bensaid, Nicolas Peltier
A Complete Superposition Calculus for Primal Grammars. J. Autom. Reason. 53 (4) (2014)
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
Decidability and Undecidability Results for Propositional Schemata. CoRR (2014)
Abdelkader Kersani, Nicolas Peltier
Combining Superposition and Induction: A Practical Realization. FroCos (2013)
Abdelkader Kersani, Nicolas Peltier
Completeness and Decidability Results for First-Order Clauses with Indices. CADE (2013)
Mnacho Echenim, Nicolas Peltier, Sophie Tourret
An Approach to Abductive Reasoning in Equational Logic. IJCAI (2013)
Mnacho Echenim, Nicolas Peltier
Instantiation Schemes for Nested Theories. ACM Trans. Comput. Log. 14 (2) (2013)
Vincent Aravantinos, Mnacho Echenim, Nicolas Peltier
A Resolution Calculus for First-order Schemata. Fundam. Informaticae 125 (2) (2013)
Cristiano Santos, Pascal Vivet, Denis Dutoit, Philippe Garrault, Nicolas Peltier, Ricardo Reis
System-level thermal modeling for 3D circuits: Characterization with a 65nm memory-on-logic circuit. 3DIC (2013)
Nicolas Peltier
Schemata of Formulæ in the Theory of Arrays. TABLEAUX (2013)
Mnacho Echenim, Nicolas Peltier
Reasoning on Schemata of Formulae CoRR (2012)
Mnacho Echenim, Nicolas Peltier
A Calculus for Generating Ground Explanations (Technical Report) CoRR (2012)
Mnacho Echenim, Nicolas Peltier
A Calculus for Generating Ground Explanations. IJCAR (2012)
Mnacho Echenim, Nicolas Peltier
Reasoning on Schemata of Formulæ. AISC/MKM/Calculemus (2012)
Nicolas Peltier, Viorica Sofronie-Stokkermans
First-order theorem proving: Foreword. J. Symb. Comput. 47 (9) (2012)
Mnacho Echenim, Nicolas Peltier
An Instantiation Scheme for Satisfiability Modulo Theories. J. Autom. Reason. 48 (3) (2012)
Vincent Aravantinos, Nicolas Peltier
Generating Schemata of Resolution Proofs CoRR (2011)
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
Linear Temporal Logic and Propositional Schemata, Back and Forth. TIME (2011)
Mnacho Echenim, Nicolas Peltier
Modular instantiation schemes. Inf. Process. Lett. 111 (20) (2011)
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
Linear Temporal Logic and Propositional Schemata, Back and Forth (extended version) CoRR (2011)
Vincent Aravantinos, Nicolas Peltier
Schemata of SMT-Problems. TABLEAUX (2011)
Mnacho Echenim, Nicolas Peltier
Instantiation Schemes for Nested Theories CoRR (2011)
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
Decidability and Undecidability Results for Propositional Schemata. J. Artif. Intell. Res. 40 (2011)
Vincent Aravantinos, Nicolas Peltier
Generating Schemata of Resolution Proofs. TABLEAUX (Workshops, Tutorials, and Short Papers) (2011)
Hicham Bensaid, Ricardo Caferra, Nicolas Peltier
-Terms in Ordered Resolution and Superposition Calculi: Retrieving Lost Completeness. AISC/MKM/Calculemus (2010)
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
Complexity of the Satisfiability Problem for a Class of Propositional Schemata. LATA (2010)
Hicham Bensaid, Ricardo Caferra, Nicolas Peltier
Perfect Discrimination Graphs: Indexing Terms with Integer Exponents. IJCAR (2010)
Nicolas Peltier
Bottom-up Construction of Semantic Tableaux. J. Log. Comput. 20 (1) (2010)
Mnacho Echenim, Nicolas Peltier
Instantiation of SMT Problems Modulo Integers. AISC/MKM/Calculemus (2010)
Mnacho Echenim, Nicolas Peltier
Instantiation of SMT problems modulo Integers CoRR (2010)
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
Simplified handling of iterated term schemata. Ann. Math. Artif. Intell. 58 (3-4) (2010)
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
RegSTAB: A SAT Solver for Propositional Schemata. IJCAR (2010)
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
A Decidable Class of Nested Iterated Schemata. IJCAR (2010)
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
A Decidable Class of Nested Iterated Schemata (extended version) CoRR (2010)
Hicham Bensaid, Ricardo Caferra, Nicolas Peltier
Dei: A Theorem Prover for Terms with Integer Exponents. CADE (2009)
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
A Schemata Calculus for Propositional Logic. TABLEAUX (2009)
Nicolas Peltier
Constructing infinite models represented by tree automata. Ann. Math. Artif. Intell. 56 (1) (2009)
Nicolas Peltier, Viorica Sofronie-Stokkermans
Preface. FTP (2009)
Rachid Echahed, Nicolas Peltier
A Needed Rewriting Strategy for Data-Structures with Pointers. RTA (2008)
Nicolas Peltier
Automated Model Building: From Finite to Infinite Models. AISC/MKM/Calculemus (2008)
Ricardo Caferra, Nicolas Peltier
Accepting/rejecting propositions from accepted/rejected propositions: A unifying overview. Int. J. Intell. Syst. 23 (10) (2008)
Nicolas Peltier
Extended resolution simulates binary decision diagrams. Discret. Appl. Math. 156 (6) (2008)
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
More Flexible Term Schematisations via Extended Primal Grammars. ISAIM (2008)
Nicolas Peltier
A Unified View of Tree Automata and Term Schematisations. IFIP TCS (2008)
Nicolas Peltier
A Bottom-Up Approach to Clausal Tableaux. TABLEAUX (2007)
Nicolas Peltier
A Resolution Calculus with Shared Literals. Fundam. Informaticae 76 (4) (2007)
Hicham Bensaid, Ricardo Caferra, Nicolas Peltier
Towards Systematic Analysis of Theorem Provers Search Spaces: First Steps. WoLLIC (2007)

Nicolas Peltier.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Nicolas Peltier