Powerlists in Coq: Programming and Reasoning. - Frédéric Loulergue; Virginia Niculescu; Simon Robillard (CANDAR, 2013)

Formal derivation and extraction of a parallel program for the all nearest smaller values problem. - Frédéric Loulergue; Simon Robillard; Julien Tesson; Joeffrey Legaux; Zhenjiang Hu (SAC, 2014)

Catamorphism Generation and Fusion Using Coq. - Simon Robillard (SYNASC, 2014)

Reasoning About Loops Using Vampire. - Laura Kovács; Simon Robillard (Vampire Workshop, 2015)

Reasoning About Loops Using Vampire in KeY. - Wolfgang Ahrendt; Laura Kovács; Simon Robillard (LPAR, 2015)

Theory-Specific Reasoning about Loops with Arrays using Vampire. - Yuting Chen; Laura Kovács; Simon Robillard (Vampire@IJCAR, 2016)

Coming to terms with quantified reasoning. - Laura Kovács; Simon Robillard; Andrei Voronkov (POPL, 2017)

Superposition with Datatypes and Codatatypes. - Jasmin Christian Blanchette; Nicolas Peltier; Simon Robillard (IJCAR, 2018)

Loop Analysis by Quantification over Iterations. - Bernhard Gleiss; Laura Kovács; Simon Robillard (LPAR, 2018)

Verified Approximation Algorithms. - Robin Eßmann; Tobias Nipkow; Simon Robillard (Arch. Formal Proofs, 2020)

Toward safe and efficient reconfiguration with Concerto. - Maverick Chardet; Hélène Coullon; Simon Robillard (Sci. Comput. Program., 2021)

Goéland: A Concurrent Tableau-Based Theorem Prover (System Description). - Julie Cailler; Johann Rosain; David Delahaye; Simon Robillard; Hinde-Lilia Bouziane (IJCAR, 2022)

SMT-Based Planning Synthesis for Distributed System Reconfigurations. - Simon Robillard; Hélène Coullon (FASE, 2022)

A Comprehensive Framework for Saturation Theorem Proving. - Uwe Waldmann; Sophie Tourret; Simon Robillard; Jasmin Blanchette (J. Autom. Reason., 2022)

Verified Approximation Algorithms. - Robin Eßmann; Tobias Nipkow; Simon Robillard; Ujkan Sulejmani (Log. Methods Comput. Sci., 2022)

DACCORD : un jeu de données pour la Détection Automatique d'énonCés COntRaDictoires en français. - Maximos Skandalis; Richard Moot; Simon Robillard (CORIA-TALN (1), 2023)

New Datasets for Automatic Detection of Textual Entailment and of Contradictions between Sentences in French. - Maximos Skandalis; Richard Moot; Christian Retoré; Simon Robillard (LREC/COLING, 2024)

An Overview of the Decentralized Reconfiguration Language Concerto-D through its Maude Formalization. - Farid Arfi; Hélène Coullon; Frédéric Loulergue; Jolan Philippe; Simon Robillard (ICE, 2024)

Component-based Distributed Software Reconfiguration:A Verification-oriented Survey. - Hélène Coullon; Ludovic Henrio; Frédéric Loulergue; Simon Robillard (ACM Comput. Surv., 2024)

Verified Path Indexing. - Mohamed Chaabani; Simon Robillard (CADE, 2025)