Generating Property-Directed Potential Invariants By Backward Analysis - Adrien Champion; Rémi Delmas; Michael Dierkes (FTSCS, 2012)

Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-linear and Linear Analyses. - Adrien Champion; Rémi Delmas; Michael Dierkes; Pierre-Loïc Garoche; Romain Jobredeaux; Pierre Roux 001 (FMICS, 2013)

Collaboration de techniques formelles pour la vérification de propriétés de sûreté sur des systèmes de transition. (Collaboration of formal techniques for the verification of safety properties over transition systems). - Adrien Champion (2014)

Generating property-directed potential invariants by quantifier elimination in a k-induction-based framework. - Adrien Champion; Rémi Delmas; Michael Dierkes (Sci. Comput. Program., 2015)

The Kind 2 Model Checker. - Adrien Champion; Alain Mebsout; Christoph Sticksel; Cesare Tinelli (CAV (2), 2016)

CoCoSpec: A Mode-Aware Contract Language for Reactive Systems. - Adrien Champion; Arie Gurfinkel; Temesghen Kahsai; Cesare Tinelli (SEFM, 2016)

HoIce: An ICE-Based Non-linear Horn Clause Solver. - Adrien Champion; Naoki Kobayashi 001; Ryosuke Sato 001 (APLAS, 2018)

ICE-Based Refinement Type Discovery for Higher-Order Functional Programs. - Adrien Champion; Tomoya Chiba; Naoki Kobayashi 001; Ryosuke Sato 001 (J. Autom. Reason., 2020)