| 2026 | IJCAR | Pgeon: Generating Tableau-Based Provers from Declarative Specifications of Logical Calculi. | Romain Sidhoum, Simon Robillard, David Delahaye |
| 2025 | CADE | Verified Path Indexing. | Mohamed Chaabani, Simon Robillard |
| 2024 | COLING | New Datasets for Automatic Detection of Textual Entailment and of Contradictions between Sentences in French. | Maximos Skandalis, Richard Moot, Christian Retor, Simon Robillard |
| 2022 | CADE | Goland: A Concurrent Tableau-Based Theorem Prover (System Description). | Julie Cailler, Johann Rosain, David Delahaye, Simon Robillard, Hinde-Lilia Bouziane |
| 2022 | FASE | SMT-Based Planning Synthesis for Distributed System Reconfigurations. | Simon Robillard, Hlne Coullon |
| 2020 | CADE | Verified Approximation Algorithms. | Robin Emann, Tobias Nipkow, Simon Robillard |
| 2020 | CADE | A Comprehensive Framework for Saturation Theorem Proving. | Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette |
| 2018 | CADE | Superposition with Datatypes and Codatatypes. | Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard |
| 2018 | LPAR | Loop Analysis by Quantification over Iterations. | Bernhard Gleiss, Laura Kovcs, Simon Robillard |
| 2017 | POPL | Coming to terms with quantified reasoning. | Laura Kovcs, Simon Robillard, Andrei Voronkov |
| 2016 | CADE | Theory-Specific Reasoning about Loops with Arrays using Vampire. | Yuting Chen, Laura Kovcs, Simon Robillard |
| 2015 | CADE | Reasoning About Loops Using Vampire. | Laura Kovcs, Simon Robillard |
| 2015 | LPAR | Reasoning About Loops Using Vampire in KeY. | Wolfgang Ahrendt, Laura Kovcs, Simon Robillard |
| 2014 | SAC | Formal derivation and extraction of a parallel program for the all nearest smaller values problem. | Frdric Loulergue, Simon Robillard, Julien Tesson, Joeffrey Legaux, Zhenjiang Hu |
| 2014 | SYNASC | Catamorphism Generation and Fusion Using Coq. | Simon Robillard |