| 2026 | CSL | On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions. | Nicolas Peltier |
| 2026 | IJCAR | A Superposition Calculus for Separation Logic. | Tanguy Bozec, Nicolas Peltier |
| 2026 | MFCS | The Entailment Problem for Separation Logic with Overlaid Structures. | Lucas Bueri, Nicolas Peltier, Quentin Petitjean, Mihaela Sighireanu |
| 2025 | WoLLIC | The Satisfiability Problem in a Separation Logic of Relations. | Nicolas Peltier |
| 2024 | IJCAR | What Is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment? | Tanguy Bozec, Nicolas Peltier, Quentin Petitjean, Mihaela Sighireanu |
| 2024 | WoLLIC | An EXPTIME-Complete Entailment Problem in Separation Logic. | Nicolas Peltier |
| 2023 | FOSSACS | A Strict Constrained Superposition Calculus for Graphs. | Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier |
| 2023 | TABLEAUX | Testing the Satisfiability of Formulas in Separation Logic with Permissions. | Nicolas Peltier |
| 2022 | TIME | Reasoning on Dynamic Transformations of Symbolic Heaps. | 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 | Superposition with Datatypes and Codatatypes. | Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard |
| 2018 | CADE | A Generic Framework for Implicate Generation Modulo Theories. | Mnacho Echenim, Nicolas Peltier, Yanis Sellami |
| 2018 | CADE | A Tableaux Calculus for Reducing Proof Size. | Michael Peter Lettmann, Nicolas Peltier |
| 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 |
| 2015 | ISLPED | A simulation framework for rapid prototyping and evaluation of thermal mitigation techniques in many-core architectures. | Tanguy Sassolas, Chiara Sandionigi, Alexandre Guerre, Julien Mottin, Pascal Vivet, Hela Boussetta, Nicolas Peltier |
| 2015 | LATA | Reasoning on Schemas of Formulas: An Automata-Based Approach. | Nicolas Peltier |
| 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 |
| 2014 | DATE | Early design stage thermal evaluation and mitigation: The locomotiv architectural case. | Tanguy Sassolas, Chiara Sandionigi, Alexandre Guerre, Alexandre Aminot, Pascal Vivet, Hela Boussetta, Luca Ferro, Nicolas Peltier |
| 2013 | CADE | Completeness and Decidability Results for First-Order Clauses with Indices. | Abdelkader Kersani, Nicolas Peltier |
| 2013 | IJCAI | An Approach to Abductive Reasoning in Equational Logic. | Mnacho Echenim, Nicolas Peltier, Sophie Tourret |
| 2013 | TABLEAUX | Schemata of Formul in the Theory of Arrays. | Nicolas Peltier |
| 2012 | AISC | Reasoning on Schemata of Formul. | Mnacho Echenim, Nicolas Peltier |
| 2012 | CADE | A Calculus for Generating Ground Explanations. | Mnacho Echenim, Nicolas Peltier |
| 2011 | TABLEAUX | Schemata of SMT-Problems. | Vincent Aravantinos, Nicolas Peltier |
| 2011 | TABLEAUX | Generating Schemata of Resolution Proofs. | Vincent Aravantinos, Nicolas Peltier |
| 2011 | TIME | Linear Temporal Logic and Propositional Schemata, Back and Forth. | Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier |
| 2010 | AISC | Untitled record | Hicham Bensaid, Ricardo Caferra, Nicolas Peltier |
| 2010 | AISC | Instantiation of SMT Problems Modulo Integers. | Mnacho Echenim, Nicolas Peltier |
| 2010 | CADE | A Decidable Class of Nested Iterated Schemata. | Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier |
| 2010 | CADE | RegSTAB: A SAT Solver for Propositional Schemata. | Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier |
| 2010 | CADE | Perfect Discrimination Graphs: Indexing Terms with Integer Exponents. | Hicham Bensaid, Ricardo Caferra, Nicolas Peltier |
| 2010 | LATA | Complexity of the Satisfiability Problem for a Class of Propositional Schemata. | Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier |
| 2009 | CADE | Dei: A Theorem Prover for Terms with Integer Exponents. | Hicham Bensaid, Ricardo Caferra, Nicolas Peltier |
| 2009 | TABLEAUX | A Schemata Calculus for Propositional Logic. | Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier |
| 2008 | AISC | Automated Model Building: From Finite to Infinite Models. | Nicolas Peltier |
| 2008 | ISAIM | More Flexible Term Schematisations via Extended Primal Grammars. | Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier |
| 2007 | TABLEAUX | A Bottom-Up Approach to Clausal Tableaux. | Nicolas Peltier |
| 2007 | WoLLIC | Towards Systematic Analysis of Theorem Provers Search Spaces: First Steps. | Hicham Bensaid, Ricardo Caferra, Nicolas Peltier |
| 2006 | PPDP | Rewriting term-graphs with priority. | Ricardo Caferra, Rachid Echahed, Nicolas Peltier |
| 2004 | JELIA | Some Techniques for Branch-Saturation in Free-Variable Tableaux. | Nicolas Peltier |
| 2003 | TABLEAUX | A More Efficient Tableaux Procedure for Simultaneous Search for Refutations and Finite Models. | Nicolas Peltier |
| 2001 | CADE | A General Method for Using Schematizations in Automated Deduction. | Nicolas Peltier |
| 2000 | CADE | Workshop: Model Computation - Principles, Algorithms, Applications. | Peter Baumgartner, Christian G. Fermller, Nicolas Peltier, Hantao Zhang |
| 1998 | CADE | System Description: An Equational Constraints Solver. | Nicolas Peltier |
| 1997 | CADE | Partial Matching for Analogy Discovery in Proofs and Counter-Examples. | Gilles Dfourneaux, Nicolas Peltier |
| 1997 | IJCAI | Analogy and Abduction in Automated Deduction. | Gilles Dfourneaux, Nicolas Peltier |
| 1997 | TABLEAUX | Simplifying and Generalizing Formulae in Tableaux. Pruning the Search Space and Building Models. | Nicolas Peltier |
| 1996 | JELIA | Building Proofs or Counterexamples by Analogy in a Resoluton Framework. | Christophe Bourely, Gilles Dfourneaux, Nicolas Peltier |
| 1995 | CSL | Decision Procedures Using Model Building Techniques. | Ricardo Caferra, Nicolas Peltier |
| 1995 | IJCAI | Extending Semantic Resolution via Automated Model Building: Applications. | Ricardo Caferra, Nicolas Peltier |
| 1995 | TABLEAUX | Model Building and Interactive Theory Discovery. | Ricardo Caferra, Nicolas Peltier |
| 1994 | CADE | A Method for Building Models Automatically. Experiments with an Extension of OTTER. | Christophe Bourely, Ricardo Caferra, Nicolas Peltier |