Catherine Dubois

According to our database, Catherine Dubois authored at least 54 papers between 1987 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2023

Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory.

Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, Ronan Saillard

CoRR, 2023

Comparing EventB, log and Why3 Models of Sparse Sets.

Maximiliano Cristiá, Catherine Dubois

CoRR, 2023

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

LibNDT: Towards a Formal Library on Spreadable Properties over Linked Nested Datatypes.

Mathieu Montin, Amélie Ledein, Catherine Dubois

Proceedings of the Proceedings Ninth Workshop on Mathematically Structured Functional Programming, 2022

A Semantics of 𝕂 into Dedukti.

Amélie Ledein, Valentin Blot, Catherine Dubois

Proceedings of the 28th International Conference on Types for Proofs and Programs, 2022

Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families.

Catherine Dubois, Nicolas Magaud, Alain Giorgetti

Proceedings of the 28th International Conference on Types for Proofs and Programs, 2022

2021

17^th Educators Symposium at MODELS 2021.

Catherine Dubois, Steffen Zschaler

Proceedings of the ACM/IEEE International Conference on Model Driven Engineering Languages and Systems Companion, 2021

2020

Formally Verified Transformation of Non-binary Constraints into Binary Constraints.

Catherine Dubois

Proceedings of the Functional and Constraint Logic Programming, 2020

2019

Teaching Formal Methods to Future Engineers.

Catherine Dubois, Virgile Prevosto, Guillaume Burel

Proceedings of the Formal Methods Teaching - Third International Workshop and Tutorial, 2019

2018

Tests and proofs for custom data generators.

Catherine Dubois, Alain Giorgetti

Formal Aspects Comput., 2018

Towards Coq Formalisation of {log} Set Constraints Resolution.

Catherine Dubois, Sulyvan Weppe

Proceedings of the 3rd International Workshop on Sets and Tools co-located with the 6th International ABZ Conference, 2018

Exploring Properties of a Telecommunication Protocol with Message Delay Using Interactive Theorem Prover.

Catherine Dubois, Olga Grinchtein, Justin Pearson, Mats Carlsson

Proceedings of the Software Engineering and Formal Methods - 16th International Conference, 2018

2017

FoCaLiZe and Dedukti to the Rescue for Proof Interoperability.

Raphaël Cauderlier, Catherine Dubois

Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

2016

Universality of Proofs (Dagstuhl Seminar 16421).

Gilles Dowek, Catherine Dubois, Brigitte Pientka, Florian Rabe

Dagstuhl Reports, 2016

Tests and Proofs for Enumerative Combinatorics.

Catherine Dubois, Alain Giorgetti, Richard Genestier

Proceedings of the Tests and Proofs - 10th International Conference, 2016

ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti.

Raphaël Cauderlier, Catherine Dubois

Proceedings of the Theoretical Aspects of Computing - ICTAC 2016, 2016

2015

Introduction.

Catherine Dubois, Régine Laleau

Tech. Sci. Informatiques, 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

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

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

Proceedings of the Proceedings 6th Workshop on Formal Methods and Analysis in SPL Engineering, 2015

Tableaux Modulo Theories Using Superdeduction.

Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois

CoRR, 2015

Termination Proofs for Recursive Functions in FoCaLiZe.

Catherine Dubois, François Pessaux

Proceedings of the Trends in Functional Programming - 16th International Symposium, 2015

2014

Objects and Subtyping in the Lambda-Pi-Calculus Modulo.

Raphaël Cauderlier, Catherine Dubois

Proceedings of the 20th International Conference on Types for Proofs and Programs, 2014

Verified Functional Iterators Using the FoCaLiZe Environment.

Catherine Dubois, Renaud Rioboo

Proceedings of the Software Engineering and Formal Methods - 12th International Conference, 2014

Formal Rule Representation and Verification from Natural Language Requirements Using an Ontology.

Driss Sadoun, Catherine Dubois, Yacine Ghamri-Doudane, Brigitte Grau

Proceedings of the Rules on the Web. From Theory to Applications, 2014

The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations.

David Delahaye, Catherine Dubois, Claude Marché, David Mentré

Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2014

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

Proceedings of the 10th International Workshop on Model Driven Engineering, 2013

From Natural Language Requirements to Formal Specification Using an Ontology.

Driss Sadoun, Catherine Dubois, Yacine Ghamri-Doudane, Brigitte Grau

Proceedings of the 25th IEEE International Conference on Tools with Artificial Intelligence, 2013

2012

A First Step in the Design of a Formally Verified Constraint-Based Testing Tool: FocalTest.

Matthieu Carlier, Catherine Dubois, Arnaud Gotlieb

Proceedings of the Tests and Proofs - 6th International Conference, 2012

ML Dependency Analysis for Assessors.

Philippe Ayrault, Vincent Benayoun, Catherine Dubois, François Pessaux

Proceedings of the Software Engineering and Formal Methods - 10th International Conference, 2012

A Certified Constraint Solver over Finite Domains.

Matthieu Carlier, Catherine Dubois, Arnaud Gotlieb

Proceedings of the FM 2012: Formal Methods, 2012

Producing Certified Functional Code from Inductive Specifications.

Pierre-Nicolas Tollitte, David Delahaye, Catherine Dubois

Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

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

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2010

FocalTest: A Constraint Programming Approach for Property-Based Testing.

Matthieu Carlier, Catherine Dubois, Arnaud Gotlieb

Proceedings of the Software and Data Technologies - 5th International Conference, 2010

Constraint Reasoning in FocalTest.

Matthieu Carlier, Catherine Dubois, Arnaud Gotlieb

Proceedings of the ICSOFT 2010, 2010

2009

Why Would You Trust B?

Éric Jaeger, Catherine Dubois

CoRR, 2009

2008

Functional Testing in the Focal Environment.

Matthieu Carlier, Catherine Dubois

Proceedings of the Tests and Proofs - 2nd International Conference, 2008

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

Extracting Purely Functional Contents from Logical Inductive Types.

David Delahaye, Catherine Dubois, Jean-Frédéric Étienne

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 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

Proceedings of the First International Conference on Research Challenges in Information Science, 2007

Why Would You Trust <i>B</i> ?

Éric Jaeger, Catherine Dubois

Proceedings of the Logic for Programming, 2007

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

A Formally Verified Geometric Modelling Core.

Catherine Dubois, Jean-Marc Mota

Proceedings of the International Conference on Software Engineering Research and Practice & Conference on Programming Languages and Compilers, 2006

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

Proceedings of the 18th Conference on Advanced Information Systems Engineering (CAiSE '06), 2006

2005

Typage, sreté et sécurité.

Catherine Dubois

Tech. Sci. Informatiques, 2005

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

Building certified components within FOCAL.

Catherine Dubois, Thérèse Hardin, Véronique Donzeau-Gouge

Proceedings of the Revised Selected Papers from the Fifth Symposium on Trends in Functional Programming, 2004

2003

Réutilisation de preuves formelles : une étude pour le système FoC.

Catherine Dubois, J. Grandguillot, Mathieu Jaume

Proceedings of the Journées francophones des langages applicatifs (JFLA'03), 2003

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

On a Generalised Logicality Theorem.

Marc Aiguier, Diane Bahrami, Catherine Dubois

Proceedings of the Artificial Intelligence, 2002

2000

Proving ML Type Soundness Within Coq.

Catherine Dubois

Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

1999

Certification of a Type Inference Tool for ML: Damas-Milner within Coq.

Catherine Dubois, Valérie Ménissier-Morain

J. Autom. Reason., 1999

1995

Generic Polymorphism.

Catherine Dubois, François Rouaix, Pierre Weis

Proceedings of the Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1995

1987

Development of a Programming Environment for Setl.

Véronique Donzeau-Gouge, Catherine Dubois, Philippe Facon, F. Jean

Proceedings of the ESEC '87, 1987