Development of a Programming Environment for Setl. - Véronique Donzeau-Gouge; Catherine Dubois; Philippe Facon; F. Jean (ESEC, 1987)

Generic Polymorphism. - Catherine Dubois; François Rouaix; Pierre Weis (POPL, 1995)

Certification of a Type Inference Tool for ML: Damas-Milner within Coq. - Catherine Dubois; Valérie Ménissier-Morain (J. Autom. Reason., 1999)

Proving ML Type Soundness Within Coq. - Catherine Dubois (TPHOLs, 2000)

On a Generalised Logicality Theorem. - Marc Aiguier; Diane Bahrami; Catherine Dubois (AISC, 2002)

Spécifications formelles du chanfreinage. - Franck Ledoux; Jean-Marc Mota; Agnès Arnould; Catherine Dubois; Pascale Le Gall; Yves Bertrand (Tech. Sci. Informatiques, 2002)

Réutilisation de preuves formelles : une étude pour le système FoC. - Catherine Dubois; J. Grandguillot; Mathieu Jaume (JFLA, 2003)

Building certified components within FOCAL. - Catherine Dubois; Thérèse Hardin; Véronique Donzeau-Gouge (Trends in Functional Programming, 2004)

Validation des règles de base de l'Atelier B. - Karim Berkani; Catherine Dubois; Alain Faivre; Jérôme Falampin (Tech. Sci. Informatiques, 2004)

Typage, sreté et sécurité. - Catherine Dubois (Tech. Sci. Informatiques, 2005)

An attempt to combine UML and formal methods to model airport security. - Yves Ledru; Régine Laleau; Michel Lemoine; Sylvie Vignes; Didier Bert; Véronique Donzeau-Gouge; Catherine Dubois; Fabien Peureux (CAiSE Forum, 2006)

A Formally Verified Geometric Modelling Core. - Catherine Dubois; Jean-Marc Mota (Software Engineering Research and Practice, 2006)

Adopting a situational requirements engineering approach for the analysis of civil aviation security standards. - Régine Laleau; Sylvie Vignes; Yves Ledru; Michel Lemoine; Didier Bert; Véronique Donzeau-Gouge; Catherine Dubois; Fabien Peureux (Softw. Process. Improv. Pract., 2006)

Why Would You Trust B ? - Éric Jaeger; Catherine Dubois (LPAR, 2007)

Using Computer Science Modeling Techniques for Airport Security Certification. - Régine Laleau; Yves Ledru; Didier Bert; Fabrice Bouquet; Michel Lemoine; Catherine Dubois; Véronique Donzeau-Gouge; Sylvie Vignes (RCIS, 2007)

Extracting Purely Functional Contents from Logical Inductive Types. - David Delahaye; Catherine Dubois; Jean-Frédéric Étienne (TPHOLs, 2007)

Raffinement de modèles topologiques en B événementiel. Des droites aux 2-G-cartes. - Jean-Marc Mota; Catherine Dubois (Tech. Sci. Informatiques, 2007)

Functional Testing in the Focal Environment. - Matthieu Carlier; Catherine Dubois (TAP, 2008)

Why Would You Trust B? - Éric Jaeger; Catherine Dubois (CoRR, 2009)

Constraint Reasoning in FocalTest. - Matthieu Carlier; Catherine Dubois; Arnaud Gotlieb (ICSOFT (2), 2010)

FocalTest: A Constraint Programming Approach for Property-Based Testing. - Matthieu Carlier; Catherine Dubois; Arnaud Gotlieb (ICSOFT (Selected Papers), 2010)

Tableaux Modulo Theories Using Superdeduction - An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover. - Mélanie Jacquel; Karim Berkani; David Delahaye; Catherine Dubois (IJCAR, 2012)

Producing Certified Functional Code from Inductive Specifications. - Pierre-Nicolas Tollitte; David Delahaye; Catherine Dubois (CPP, 2012)

A Certified Constraint Solver over Finite Domains. - Matthieu Carlier; Catherine Dubois; Arnaud Gotlieb (FM, 2012)

ML Dependency Analysis for Assessors. - Philippe Ayrault; Vincent Benayoun; Catherine Dubois; François Pessaux (SEFM, 2012)

A First Step in the Design of a Formally Verified Constraint-Based Testing Tool: FocalTest. - Matthieu Carlier; Catherine Dubois; Arnaud Gotlieb (TAP@TOOLS, 2012)

From Natural Language Requirements to Formal Specification Using an Ontology. - Driss Sadoun; Catherine Dubois; Yacine Ghamri-Doudane; Brigitte Grau (ICTAI, 2013)

Research Questions for Validation and Verification in the Context of Model-Based Engineering. - Catherine Dubois; Michalis Famelis; Martin Gogolla; Leonel Nóbrega; Ileana Ober; Martina Seidl; Markus Völter (MoDeVVa@MoDELS, 2013)

The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations. - David Delahaye; Catherine Dubois; Claude Marché; David Mentré (ABZ, 2014)

Formal Rule Representation and Verification from Natural Language Requirements Using an Ontology. - Driss Sadoun; Catherine Dubois; Yacine Ghamri-Doudane; Brigitte Grau (RuleML, 2014)

Verified Functional Iterators Using the FoCaLiZe Environment. - Catherine Dubois; Renaud Rioboo (SEFM, 2014)

Objects and Subtyping in the Lambda-Pi-Calculus Modulo. - Raphaël Cauderlier; Catherine Dubois (TYPES, 2014)

Termination Proofs for Recursive Functions in FoCaLiZe. - Catherine Dubois; François Pessaux (TFP, 2015)

Tableaux Modulo Theories Using Superdeduction. - Mélanie Jacquel; Karim Berkani; David Delahaye; Catherine Dubois (CoRR, 2015)

Towards correct-by-construction product variants of a software product line: GFML, a formal language for feature modules. - Thi-Kim-Zung Pham; Catherine Dubois; Nicole Lévy (FMSPLE, 2015)

Représentation et vérification d'un environnement intelligent à partir de spécifications utilisateur en langage naturel. - Driss Sadoun; Catherine Dubois; Yacine Ghamri-Doudane; Brigitte Grau (Rev. d'Intelligence Artif., 2015)

Verifying B proof rules using deep embedding and automated theorem proving. - Mélanie Jacquel; Karim Berkani; David Delahaye; Catherine Dubois (Softw. Syst. Model., 2015)

Introduction. - Catherine Dubois; Régine Laleau (Tech. Sci. Informatiques, 2015)

ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti. - Raphaël Cauderlier; Catherine Dubois (ICTAC, 2016)

Tests and Proofs for Enumerative Combinatorics. - Catherine Dubois; Alain Giorgetti; Richard Genestier (TAP@STAF, 2016)

Universality of Proofs (Dagstuhl Seminar 16421). - Gilles Dowek; Catherine Dubois; Brigitte Pientka; Florian Rabe 001 (Dagstuhl Reports, 2016)

FoCaLiZe and Dedukti to the Rescue for Proof Interoperability. - Raphaël Cauderlier; Catherine Dubois (ITP, 2017)

Exploring Properties of a Telecommunication Protocol with Message Delay Using Interactive Theorem Prover. - Catherine Dubois; Olga Grinchtein; Justin Pearson; Mats Carlsson (SEFM, 2018)

Towards Coq Formalisation of {log} Set Constraints Resolution. - Catherine Dubois; Sulyvan Weppe (SETS@ABZ, 2018)

Tests and proofs for custom data generators. - Catherine Dubois; Alain Giorgetti (Formal Aspects Comput., 2018)

Teaching Formal Methods to Future Engineers. - Catherine Dubois; Virgile Prevosto; Guillaume Burel (FMTea, 2019)

Formally Verified Transformation of Non-binary Constraints into Binary Constraints. - Catherine Dubois (WFLP, 2020)

17th Educators Symposium at MODELS 2021. - Catherine Dubois; Steffen Zschaler (MoDELS (Companion), 2021)

Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families. - Catherine Dubois; Nicolas Magaud; Alain Giorgetti (TYPES, 2022)

A Semantics of 𝕂 into Dedukti. - Amélie Ledein; Valentin Blot; Catherine Dubois (TYPES, 2022)

LibNDT: Towards a Formal Library on Spreadable Properties over Linked Nested Datatypes. - Mathieu Montin; Amélie Ledein; Catherine Dubois (MSFP@ETAPS, 2022)

Automatic Synthesis of Random Generators for Numerically Constrained Algebraic Recursive Types. - Ghiles Ziat; Vincent Botbol; Matthieu Dien; Arnaud Gotlieb; Martin Pépin; Catherine Dubois (CoRR, 2022)

Comparing EventB, log and Why3 Models of Sparse Sets. - Maximiliano Cristiá; Catherine Dubois (CoRR, 2023)

Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory. - Ali Assaf 002; Guillaume Burel; Raphaël Cauderlier; David Delahaye; Gilles Dowek; Catherine Dubois; Frédéric Gilbert 002; Pierre Halmagrand; Olivier Hermant; Ronan Saillard (CoRR, 2023)

Deductive Verification of Sparse Sets in Why3. - Catherine Dubois (VSTTE, 2024)

On Formal Methods Thinking in Computer Science Education. - Brijesh Dongol; Catherine Dubois; Stefan Hallerstede; Eric C. R. Hehner; Carroll Morgan; Peter Müller 001; Leila Ribeiro 001; Alexandra Silva 001; Graeme Smith 001; Erik P. de Vink (Formal Aspects Comput., 2025)