SAMOVAR - SAMOVAR
Telecom SudParis
9 rue Charles Fourier
91011 EVRY CEDEX

Fax : +33 (0) 1 60 76 20 80

Pr. Catherine DUBOIS

Professeur
ACMES

catherine.dubois[@-Code to remove to avoid SPAM-]ensiie.fr

Article dans une revue

2018

ref_biblio
Catherine Dubois, Alain Giorgetti. Tests and proofs for custom data generators. Formal Aspects of Computing, 2018, 30 (6), pp.659 - 684. ⟨hal-02302096⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02302096/file/34629641-d48a-4e33-a475-164f13aa918f-author.pdf BibTex

2016

ref_biblio
Catherine Dubois, Genevieve Cloutier, Maja Rosenkilde Rynning, Luc Adolphe, Marion Bonhomme. City and Building Designers, and Climate Adaptation. Buildings, 2016, 6 (3), pp.28. ⟨10.3390/buildings6030028⟩. ⟨hal-02155859⟩
Accès au texte intégral et bibtex
https://insa-toulouse.hal.science/hal-02155859/file/2016_Buildings.pdf BibTex

2015

ref_biblio
Catherine Dubois, Régine Laleau. Introduction. Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, 2015, 34 (5), pp.493--494. ⟨hal-01575305⟩
Accès au bibtex
BibTex
ref_biblio
Catherine Dubois, Genevieve Cloutier, Andre Potvin, Luc Adolphe, Florent Joerin. Design support tools to sustain climate change adaptation at the local level: A review and reflection on their suitability. Frontiers of architectural research, 2015, 4 (1), pp.1--11. ⟨10.1016/j.foar.2014.12.002⟩. ⟨hal-01849770⟩
Accès au texte intégral et bibtex
https://insa-toulouse.hal.science/hal-01849770/file/1-s2.0-S2095263514000752-main.pdf BibTex
ref_biblio
Driss Sadoun, Catherine Dubois, Yacine Ghamri-Doudane, Brigitte Grau. Représentation et vérification d’un environnement intelligent à partir de spécifications utilisateur en langage naturel. Revue des Sciences et Technologies de l'Information - Série RIA : Revue d'Intelligence Artificielle, 2015, 29 (1), pp.47-81. ⟨10.3166/RIA.29.47-81⟩. ⟨hal-01378061⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01378061/file/RIA2015-auteur.pdf BibTex

2012

ref_biblio
Karim Berkani, David Delahaye, Catherine Dubois, Mélanie Jacquel, Martin Keogh, et al.. BCARe : un environnement pour la vérification de règles de l'Atelier B. Approches Formelles dans l'Assistance au Développement de Logiciels, 2012, pp.46-49. ⟨hal-00722385⟩
Accès au bibtex
BibTex

2011

ref_biblio
Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois. Verifying B Proof Rules using Deep Embedding and Automated Theorem Proving. Software Engineering and Formal Methods, 2011, 7041, pp.253-268. ⟨10.1007/978-3-642-24690-6_18⟩. ⟨hal-00722373⟩
Accès au bibtex
BibTex

2009

ref_biblio
Jerôme Lafont, Hélène Thibout, Catherine Dubois, Maryvonne Laurent, Cécile Martinerie. NOV/CCN3 Induces Adhesion of Muscle Skeletal Cells and Cooperates with FGF2 and IGF-1 to Promote Proliferation and Survival. Cell Communication and Adhesion, 2009, 12 (1-2), pp.41-57. ⟨10.1080/15419060500383069⟩. ⟨hal-03824123⟩
Accès au bibtex
BibTex

2008

ref_biblio
Catherine Dubois, Jean Noël Ravey, J.B Noël, Laurence Pittet-Barbier, Gilbert R. Ferretti. [Creation and development of a website on imaging of bone tumors]. Journal de Radiologie, 2008, 89 (2), pp.264-6. ⟨inserm-00335705⟩
Accès au bibtex
BibTex
ref_biblio
Noélie Hohn, Dimitri Salameire, Christophe M. Pison, Catherine Dubois, Gilbert R. Ferretti. [Dense spontaneous bronchogram]. Revue des Maladies Respiratoires, 2008, 25 (5), pp.619-21. ⟨inserm-00335715⟩
Accès au bibtex
BibTex

2007

ref_biblio
Emilie Droeven, Catherine Dubois, Claude Feltz. Paysages patrimoniaux en Wallonie (Belgique), analyse par approche des paysages témoins. Cahiers d'Economie et de Sociologie Rurales, 2007, 84-85, pp.215-244. ⟨hal-01201155⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01201155/file/84-85-215-244.pdf BibTex
ref_biblio
Jean Marc Mota, Catherine Dubois. Raffinement de modèles topologiques : des droites aux 2-G-cartes. Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, 2007, 26, pp.883-908. ⟨hal-01125402⟩
Accès au bibtex
BibTex

2006

ref_biblio
Frederico Calhabeu, Jérome Lafont, Gwenvael Le Dreau, Maryvonne Laurent, Chantal Kazazian, et al.. NOV/CCN3 impairs muscle cell commitment and differentiation. Experimental Cell Research, 2006, 312 (10), pp.1876-1889. ⟨10.1016/j.yexcr.2006.02.027⟩. ⟨hal-03824115⟩
Accès au bibtex
BibTex
ref_biblio
Régine Laleau, Sylvie Vignes, Yves Ledru, Michel Lemoine, Didier Bert, et al.. Adopting a situational requirements engineering approach for the analysis of civil aviation security standards. Software Process: Improvement and Practice, 2006, 11 (5), pp.487-503. ⟨hal-00147053⟩
Accès au bibtex
BibTex

2005

ref_biblio
Catherine Dubois. Typage, sûreté et sécurité. Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, 2005, 24, pp.1187-1190. ⟨hal-01125404⟩
Accès au bibtex
BibTex
ref_biblio
Jerome Lafont, Claire Jacques, Gwenvael Le Dreau, Frederico Calhabeu, Helene Thibout, et al.. New Target Genes for NOV/CCN3 in Chondrocytes: TGF-β2 and Type X Collagen. Journal of Bone and Mineral Research, 2005, 20 (12), pp.2213-2223. ⟨10.1359/JBMR.050818⟩. ⟨hal-03824118⟩
Accès au bibtex
BibTex

2004

ref_biblio
Karim Berkani, Catherine Dubois, Alain Faivre, J?r?me Falampin. Validation des règles de base de l'Atelier B. Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, 2004, 23, pp.855-878. ⟨hal-01124962⟩
Accès au bibtex
BibTex

2002

ref_biblio
Franck Ledoux, Jean-Marc Mota, Agnès Arnould, Catherine Dubois, Pascale Le Gall, et al.. Spécifications formelles du chanfreinage. Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, 2002, 21 (8), pp.1-26. ⟨hal-00352083⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00352083/file/TSI2001_2.pdf BibTex

Communication dans un congrès

2024

ref_biblio
Maximiliano Cristiá, Catherine Dubois. Comparing EventB, {log} and Why3 Models of Sparse Sets. 35es Journées Francophones des Langages Applicatifs (JFLA 2024), Jan 2024, Saint-Jacut-de-la-Mer, France. ⟨hal-04407130⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04407130/file/jfla2024-paper-71.pdf BibTex

2023

ref_biblio
Catherine Dubois, Nicolas Magaud, Alain Giorgetti. Pragmatic isomorphism proofs between Coq representations: application to lambda-term families. 28th International Conference on Types for Proofs and Programs (TYPES 2022), Nantes, France, Jan 2023, Nantes, France. ⟨hal-04094291⟩
Accès au bibtex
BibTex
ref_biblio
Amélie Ledein, Valentin Blot, Catherine Dubois. A semantics of K into dedukti. TYPES 2022 - 28th International Conference on Types for Proofs and Programs (TYPES), Jul 2023, Nantes, France. ⟨10.4230/LIPIcs.TYPES.2022.23⟩. ⟨hal-03895834v2⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03895834/file/LIPIcs.TYPES.2022.12.pdf BibTex

2022

ref_biblio
Catherine Dubois, Nicolas Magaud, Alain Giorgetti. Pragmatic isomorphism proofs between coq representations: application to lambda-term families. 28th International Conference on Types for Proofs and Programs (TYPES 2022), Jun 2022, Nantes, France. pp.11:1-11:19, ⟨10.4230/LIPIcs.TYPES.2022.11⟩. ⟨hal-04245455⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04245455/file/906251f5-cd51-46c3-98a7-79cb0b561fbc-author.pdf BibTex
ref_biblio
Amélie Ledein, Valentin Blot, Catherine Dubois. Vers une traduction de K en Dedukti. JFLA 2022 - Journées Francophones des Langages Applicatifs (JFLA), Jun 2022, Saint-Médard-d'Excideuil, France. ⟨hal-03604962⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03604962/file/jfla22_paper_7.pdf BibTex
ref_biblio
Mathieu Montin, Amélie Ledein, Catherine Dubois. LibNDT: towards a formal library on spreadable properties over linked nested datatypes. Ninth Workshop on Mathematically Structured Functional Programming (MSFP), Jeremy Gibbons; Max S. New, Apr 2022, Munich, Germany. pp.27-44, ⟨10.4204/eptcs.360.2⟩. ⟨hal-04316452⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04316452/file/liblndt.pdf BibTex
ref_biblio
Ghiles Ziat, Vincent Botbol, Matthieu Dien, Arnaud Gotlieb, Martin Pépin, et al.. Automatic synthesis of random generators for numerically constrained algebraic recursive types. 32nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2022), Sep 2022, Tbilisi, Georgia. ⟨10.48550/arXiv.2208.12747⟩. ⟨hal-04551862⟩
Accès au bibtex
https://arxiv.org/pdf/2208.12747 BibTex

2020

ref_biblio
Catherine Dubois. Formally verified transformation of non-binary constraints into binary constraints. International Workshop on Functional and Constraint Logic Programming (WFLP), Sep 2020, Bologna, Italy. pp.117-128, ⟨10.1007/978-3-030-75333-7_7⟩. ⟨hal-04330062⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04330062/file/wflp2020_final.pdf BibTex
ref_biblio
Amélie Ledein, Catherine Dubois. FaCiLe en Coq : vérification formelle des listes d'intervalles. Les 31es Journées Francophones des Langages Applicatifs (JFLA), Jan 2020, Gruisan, France. ⟨hal-04344249⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04344249/file/paper_17.pdf BibTex

2019

ref_biblio
Catherine Dubois, Virgile Prévosto, Guillaume Burel. Teaching formal methods to future engineers. Third International Workshop and Tutorial, FMTea, Sep 2019, Porto, Portugal. pp.69-80, ⟨10.1007/978-3-030-32441-4_5⟩. ⟨cea-02874103⟩
Accès au texte intégral et bibtex
https://cea.hal.science/cea-02874103/file/Teaching_Formal_Methods_to_Engineers.pdf BibTex
ref_biblio
Alain Giorgetti, Catherine Dubois, Rémi Lazarini. Combinatoire formelle avec Why3 et Coq. Journées Francophones des Langages Applicatifs (JFLA), Jan 2019, Les Rousses, France. ⟨hal-02302086⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02302086/file/970c0f52-c8e5-46fb-a50f-b117ee9075bd-author%20%281%29.pdf BibTex

2018

ref_biblio
Catherine Dubois, Olga Grinchtein, Justin Pearson, Mats Carlsson. Exploring properties of a telecommunication protocol with message delay using interactive theorem prover. International Conference on Software Engineering and Formal Methods (SEFM), Jun 2018, Toulouse, France. pp.239-253, ⟨10.1007/978-3-319-92970-5_15⟩. ⟨hal-04489907⟩
Accès au bibtex
BibTex

2017

ref_biblio
Luc Adolphe, Benjamin Rousval, Tathiane Martins, Marion Bonhomme, Catherine Dubois. Towards new design tools for integrating environmental criteria in the design process of architectural and urban projects in developing countries. 30ème conférence PLEA (Passive Low Energy Architecture), Dec 2017, Ahmedabad, India. ⟨hal-02157305⟩
Accès au texte intégral et bibtex
https://insa-toulouse.hal.science/hal-02157305/file/PLEA2014_Adolphe.pdf BibTex
ref_biblio
Raphaël Cauderlier, Catherine Dubois. FoCaLiZe and Dedukti to the rescue for proof interoperability. ITP 2017: International Conference on Interactive Theorem Proving, Sep 2017, Brasília, Brazil. pp.532, ⟨10.1007/978-3-319-66107-0_9⟩. ⟨hal-01592243v2⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01592243/file/article%20%281%29.pdf BibTex
ref_biblio
Thi-Kim-Zung Pham, Catherine Dubois, Nicole Levy. Une ligne de produits corrects par construction. AFADL 2017: 6èmes journées des Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2017, Montpellier, France. pp.79 - 85. ⟨hal-01670764⟩
Accès au bibtex
BibTex

2016

ref_biblio
Ali Assaf, Guillaume Burel, Raphal Cauderlier, David Delahaye, Gilles Dowek, et al.. Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system. TYPES: Types for Proofs and Programs, May 2016, Novi SAd, Serbia. ⟨hal-01441751⟩
Accès au texte intégral et bibtex
https://minesparis-psl.hal.science/hal-01441751/file/A-654.pdf BibTex
ref_biblio
Raphaël Cauderlier, Catherine Dubois. ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti. ICTAC 2016 - 13th International Colloquium on Theoretical Aspects of Computing, Oct 2016, Taipei, Taiwan. pp.459-468, ⟨10.1007/978-3-319-46750-4_26⟩. ⟨hal-01420638⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01420638/file/ICTAC_2016.pdf BibTex
ref_biblio
Catherine Dubois, Alain Giorgetti, Richard Genestier. Tests and proofs for enumerative combinatorics. TAP 2016: International Conference on Tests and Proofs, Jul 2016, Vienna, Austria. pp.57-75, ⟨10.1007/978-3-319-41135-4_4⟩. ⟨hal-01670709⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01670709/file/TPEC2016.pdf BibTex
ref_biblio
Catherine Dubois, Antonin Butant, Sourour Elloumi. Preuve formelle et contrainte alldiff. ROADEF 2016 : 17e conférence de la société française de Recherche Opérationnelle et d'Aide à la Décision, Feb 2016, Compiègne, France. pp.1 - 2. ⟨hal-01670972⟩
Accès au bibtex
BibTex

2015

ref_biblio
Marion Bonhomme, Catherine Dubois, Luc Adolphe, Genevieve Cloutier, Serge Faraut, et al.. The CapaCities project: from Concepts to Actions for a Proactive Adaptation of Cities. 9ème conférence ICUC (International Conference on Urban Climate), Jul 2015, Toulouse, France. ⟨hal-02157093⟩
Accès au bibtex
BibTex
ref_biblio
Catherine Dubois, Sourour Elloumi, Benoit Robillard, Clément Vincent. Graphes et couplages en Coq. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. ⟨hal-01099140⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01099140/file/jfla15_submission_36.pdf BibTex
ref_biblio
Alain Giorgetti, Catherine Dubois, Noam Zeilberger. Lambda terms and maps, formally. Workshop on Computational Logic and Applications, Mar 2015, Lyon, France. ⟨hal-03221915⟩
Accès au bibtex
BibTex
ref_biblio
Thi-Kim-Zung Pham, Catherine Dubois, Nicole Lévy. Towards correct-by-construction product variants of a software product line: GFML, a formal language for feature modules. 6th Workshop on Formal Methods and Analysis in SPL Engineering (FMSPLE), Apr 2015, London, United Kingdom. pp.44-55, ⟨10.4204/EPTCS.182.4⟩. ⟨lirmm-02464897⟩
Accès au texte intégral et bibtex
https://hal-lirmm.ccsd.cnrs.fr/lirmm-02464897/file/PDL15.pdf BibTex
ref_biblio
Driss Sadoun, Catherine Dubois, Yacine Ghamri-Doudane, Brigitte Grau. Configuration en langue naturelle du fonctionnement d'une maison intelligente. 14èmes journées Approches Formelles dans l'Assistance au Développement Logiciel, AFADL,, Jun 2015, Bordeaux, France. ⟨hal-01378152⟩
Accès au bibtex
BibTex

2014

ref_biblio
Raphaël Cauderlier, Ali Assaf, Catherine Dubois. Objects and subtyping in the lambda-Pi-calculus modulo. TYPES 2014, May 2014, Paris, France. pp.2. ⟨hal-01126394⟩
Accès au bibtex
BibTex
ref_biblio
David Delahaye, Catherine Dubois, Claude Marché, David Mentré. The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations. Abstract State Machines, Alloy, B, VDM, and Z, Jun 2014, Toulouse, France. pp.290-293. ⟨hal-00998092⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00998092/file/bware_ABZ_14_.pdf BibTex
ref_biblio
Catherine Dubois, Renaud Rioboo. Verified functional iterators using the FoCaLiZe environment. Software Engineering and Formal Methods, Sep 2014, X, France. pp.317--331. ⟨hal-01126458⟩
Accès au bibtex
BibTex
ref_biblio
Driss Sadoun, Catherine Dubois, Yacine Ghamri-Doudane, Brigitte Grau. Formal Rule Representation and Verification from Natural Language Requirements Using an Ontology. RuleML, Aug 2014, Prague, Czech Republic. pp.226-235, ⟨10.1007/978-3-319-09870-8_17⟩. ⟨hal-01126517⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01126517/file/RuleML.pdf BibTex

2013

ref_biblio
David Delahaye, Catherine Dubois, Pierre-Nicolas Tollitte. RelExt : Synthèse de code à partir de spécifications inductives. AFADL 2013, Apr 2013, Nancy, France. 4 p. ⟨hal-01126320⟩
Accès au bibtex
BibTex
ref_biblio
Catherine Dubois, Michalis Famelis, Martin Gogolla, Leonel Nobrega, Ileana Ober, et al.. Research Questions for Validation and Verification in the Context of Model-Based Engineering. International Workshop on Model Driven Engineering, Verification and Validation - MoDeVVA 2013, Oct 2013, Miami, United States. pp. 67-76. ⟨hal-01144308⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01144308/file/Dubois_12880.pdf BibTex
ref_biblio
Catherine Dubois, Arnaud Gotlieb. Solveurs CP(FD) vérifiés formellement. Neuvi?mes Journ?es Francophones de Programmation par Contraintes (JFPC 2013), Jun 2013, Aix-en-Provence, France. pp.115-118. ⟨hal-01126318⟩
Accès au bibtex
BibTex
ref_biblio
Driss Sadoun, Catherine Dubois, Yacine Ghamri-Doudane, Brigitte Grau. Peuplement d’une ontologie guidé par l’identification d’instances de propriété. 10th International Conference on Terminology and Artificial Intelligence (TIA'2013), Oct 2013, Paris, France. pp.145-152. ⟨hal-02296903⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02296903/file/tia-publie.pdf BibTex
ref_biblio
Driss Sadoun, Catherine Dubois, Yacine Ghamri-Doudane, Brigitte Grau. From Natural Language Requirements to Formal Specification Using an Ontology. IEEE 25th International Conference on Tools with Artificial Intelligence (ICTAI 2013), Nov 2013, Herndon, VA, United States. pp.755-760, ⟨10.1109/ICTAI.2013.116⟩. ⟨hal-01126372⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01126372/file/ictai2013.pdf BibTex

2012

ref_biblio
Karim Berkani, David Delahaye, Catherine Dubois, Mélanie Jacquel, Martin Keogh, et al.. BCARe : un environnement pour la vérification de règles de l?Atelier B. Approches Formelles dans l'Assistance au D?veloppement de Logiciels (AFADL 2012), Jan 2012, Grenoble, France. pp.46-49. ⟨hal-01126033⟩
Accès au bibtex
BibTex
ref_biblio
Matthieu Carlier, Catherine Dubois, Arnaud Gotlieb. A first step in the design of a formally verified constraint-based testing tool: FocalTest. Tests and Proofs, May 2012, Prague, Czech Republic. pp.35--50. ⟨hal-01126115⟩
Accès au bibtex
BibTex
ref_biblio
Matthieu Carlier, Catherine Dubois, Arnaud Gotlieb. A certified constraint solver over finite domains. Formal Methods (FM 2012) (ex FME), Aug 2012, Paris, France. pp.116-131. ⟨hal-01126135⟩
Accès au bibtex
BibTex
ref_biblio
Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois. Tableaux Modulo Theories using Superdeduction: An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover. International Joint Conference on Automated Reasoning (IJCAR 2012), Jun 2012, Manchester, Ukraine. pp.332--338. ⟨hal-01126134⟩
Accès au bibtex
BibTex
ref_biblio
Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois. Tableaux Modulo Theories Using Superdeduction. IJCAR 2012 - 6th International Joint Conference on Automated Reasoning, Jun 2012, Manchester, UK, United Kingdom. pp.1 - 13, ⟨10.1007/978-3-642-31365-3_26⟩. ⟨hal-01099338⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01099338/file/tab-sded.pdf BibTex
ref_biblio
François Pessaux, Vincent Benayoun, Catherine Dubois, Philippe Ayrault. ML Dependency Analysis for Assessors. Software Engineering and Formal Methods (SEFM) 2012, Oct 2012, Thessaloniki, Greece. pp.278-292, ⟨10.1007/978-3-642-33826-7_19⟩. ⟨hal-01203505⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01203505/file/ML_deps_assess.pdf BibTex
ref_biblio
Driss Sadoun, Catherine Dubois, Yacine Ghamri-Doudane, Brigitte Grau. Formalisation en OWL pour vérifier les spécifications d'un environnement intelligent. RFIA 2012 (Reconnaissance des Formes et Intelligence Artificielle), Jan 2012, Lyon, France. pp.978-2-9539515-2-3. ⟨hal-00656526⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00656526/file/rfia2012_submission_117.pdf BibTex
ref_biblio
Pierre-Nicolas Tollitte, David Delahaye, Catherine Dubois. Producing Certified Functional Code from Inductive Specifications. International Conference on Certified Programs and Proofs (CPP 2012), Dec 2012, Kyoto, Japan. pp.76-91. ⟨hal-01126212⟩
Accès au bibtex
BibTex

2011

ref_biblio
Catherine Dubois. Tutorial: introduction to Coq. TOOLS 2011, Jun 2011, Zurich, Switzerland. ⟨hal-01126146⟩
Accès au bibtex
BibTex
ref_biblio
Driss Sadoun, Catherine Dubois, Yacine Ghamri-Doudane, B. Grau. An ontology for the conceptualization of an intelligent environment and its operation. 10th Mexican International Conference on Artificial Intelligence (MICAI 2011), Nov 2011, Puebla, Mexico. ⟨10.1109/MICAI.2011.32⟩. ⟨hal-00808002⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00808002/file/Conceptualization_of_intelligent_environment.pdf BibTex

2010

ref_biblio
Mathieu Carlier, Catherine Dubois, Arnaud Gotlieb. Constraint Reasoning in FocalTest. ICSOFT, Jul 2010, Athènes, Greece. ⟨hal-00699233⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00699233/file/paper.pdf BibTex
ref_biblio
David Delahaye, Catherine Dubois, Pierre-Nicolas Tollitte. Génération de code fonctionnel certifié à partir de spécifications inductives dans l'environnement Focalize. Journ?es Francophones des Langages Applicatifs (JFLA'10), Jan 2010, La Ciotat, France. pp.55-81. ⟨hal-01125723⟩
Accès au bibtex
BibTex

2009

ref_biblio
Matthieu Carlier, Catherine Dubois, Lionel Habib, Mathieu Jaume. Politique de contrôle d'accès multi-niveaux : test de conformité vis à vis des flots avec l'outil FoCaL. AFADL'09 - Approches formelles dans l'assistance au développement des Logiciels, Jan 2009, Toulouse, France. pp.145-160. ⟨hal-01125619⟩
Accès au bibtex
BibTex

2008

ref_biblio
Philippe Ayrault, Matthieu Carlier, David Delahaye, Catherine Dubois, Damien Doligez, et al.. Trusted Software within Focal. C&ESAR 2008 - Computer & Electronics Security Applications Rendez-vous, Dec 2008, Rennes, France. pp.162-179. ⟨hal-01125667v2⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01125667/file/cesar.pdf BibTex
ref_biblio
Catherine Dubois, Matthieu Carlier. Functional Testing in the Focal environment. Tests and Proofs (TAP 2008), Apr 2008, Prato, Italy. pp.84-98. ⟨hal-01125411⟩
Accès au bibtex
BibTex

2007

ref_biblio
David Delahaye, Catherine Dubois, Jean-Frédéric Etienne. Extracting Purely Functional Contents from Logical Inductive Types. TPHOLs'07 Theorem Proving in Higher Order Logics, Kaiserslautern (Germany), Jan 2007, X, France. pp.70-85. ⟨hal-01125370⟩
Accès au bibtex
BibTex
ref_biblio
Eric Jaeger, Catherine Dubois. Why Would You Trust B?. Logic for Programming, Artificial Intelligence, and Reasoning, Nov 2007, Yerevan, Armenia. pp.288-302, ⟨10.1007/978-3-540-75560-9⟩. ⟨hal-00363345⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00363345/file/BiCoq.pdf BibTex
ref_biblio
Régine Laleau, Yves Ledru, Didier Bert, Fabrice Bouquet, Michel Lemoine, et al.. Using Computer Science Modeling Techniques for Airport Security Certification. RCIS''07 First Int. Conf. on Research Challenges in Information Science, Ouarzazate, Jan 2007, X, France. pp.61-72. ⟨hal-01125403⟩
Accès au bibtex
BibTex

2006

ref_biblio
Catherine Dubois, Jean-Marc Mota. A formally verified geometric modelling core. SERP'06 - Int. Conf. on Software Engineering Research and Practice, Las Vegas, USA,, Jan 2006, X, France. pp.643-649. ⟨hal-01125234⟩
Accès au bibtex
BibTex
ref_biblio
Yves Ledru, Régine Laleau, Michel Lemoine, Sylvie Vignes, Didier Bert, et al.. An attempt to combine UML and formal methods to model airport security. CAISE’06 Forum, Jan 2006, X, France. ⟨hal-01125236⟩
Accès au bibtex
BibTex
ref_biblio
Jean-Marc Mota, Catherine Dubois. Raffinement de données en B événementiel pour les algorithmes géométriques. AFADL'06 - Approches Formelles dans l'Assistance au Développement de Logiciels, Paris, France. 200, Jan 2006, X, France. ⟨hal-01125235⟩
Accès au bibtex
BibTex

2005

ref_biblio
Régine Laleau, Sylvie Vignes, Yves Ledru, Michel Lemoine, Didier Bert, et al.. Application of Requirements Engineering Techniques to the Analysis of Civil Aviation Security Standards. SREP'05 International Workshop, In conjunction with 13th IEEE International Requirements Engineering, Jan 2005, X, France. ⟨hal-01125097⟩
Accès au bibtex
BibTex
ref_biblio
Régine Laleau, Sylvie Vignes, Yves Ledru, Michel Lemoine, Didier Bert, et al.. Application of Requirements Analysis Techniques to the analysis of civil aviation security standards. SREP'05 - Proceedings of the First International Workshop on Situational Requirements Engineering Processes: Methods, Techniques and Tools to Support Situation-Specific Requirements Engineering Processes. Organized by IFIP WG8.1 Method Engineering Task Group, In conjunction with the 13th IEEE International Requirements Engineering Conference, 2005, Paris, France. pp.91--106. ⟨hal-01224666⟩
Accès au bibtex
BibTex

2004

ref_biblio
Catherine Dubois, Thérèse Hardin, Véronique Viguie Donzeau Gouge. Building certified components within FOCAL. TFP 2004 - 5th Symposium on Trends in Functional Programming, Nov 2004, Munich, Germany. pp.33-48. ⟨hal-01520668⟩
Accès au bibtex
BibTex
ref_biblio
Catherine Dubois, Mathieu Jaume, Olivier Pons, Virgile Prévosto. L'atelier Focal. AFADL, session outils, Jan 2004, X, France. ⟨hal-01125052⟩
Accès au bibtex
BibTex

2003

ref_biblio
Karim Berkani, Catherine Dubois, Alain Faivre, J?r?me Falampin. Validation des règles de base de l'Atelier B. AFADL'03, Jan 2003, X, France. ⟨hal-01124791⟩
Accès au bibtex
BibTex
ref_biblio
Catherine Dubois, Jérôme Grandguillot, Mathieu Jaume. Réutilisation de preuves - Une étude pour le système Foc. Journées francophones des langages applicatifs, Jan 2003, X, France. ⟨hal-01124792⟩
Accès au bibtex
BibTex
ref_biblio
Catherine Dubois, Jérôme Grandguillot, Mathieu Jaume. Réutilisation de preuves formelles : une étude pour le système Foc. Journées Francophones des Langages Applicatifs, JFLA'03, Jan 2003, Chamrousse, France. pp.63-76. ⟨hal-01530419⟩
Accès au bibtex
BibTex

2001

ref_biblio
Olivier Boite, Catherine Dubois. Proving Type Soundness of a Simply Typed ML-like Language with References. TPHOLs2001, Jan 2001, X, France. ⟨hal-01124763⟩
Accès au bibtex
BibTex
ref_biblio
F. Ledoux, Jean-Marc Mota, A. Arnould, Catherine Dubois, P. Le Gall, et al.. Spécifications formelles du chanfreinage. AFADL2001, Jan 2001, X, France. ⟨hal-01124624⟩
Accès au bibtex
BibTex

2000

ref_biblio
M. Aiguier, D. Bahrami, Catherine Dubois. Axioms for Rewriting Theory. PLI 2000, Workshop RULE 2000 : First International Workshop on Rule-Based Programming Montreal, Cana, Jan 2000, X, France. ⟨hal-01124623⟩
Accès au bibtex
BibTex

Chapitre d'ouvrage

2004

ref_biblio
Catherine Dubois, Valerie Menissier-Morain. Apprentissage de la programmation avec OCaml. Apprentissage de la programmation avec OCaml, 2004. ⟨hal-01124971⟩
Accès au bibtex
BibTex

N°spécial de revue/special issue

2017

ref_biblio
Catherine Dubois, Paolo Masci, Dominique Méry. Proceedings of the Third Workshop on Formal Integrated Development Environment, F-IDE@FM 2016, Limassol, Cyprus, November 8, 2016. Nov 2016, Cyprus. Electronic Proceedings in Theoretical Computer Science, 240, 2017, ⟨10.4204/EPTCS.240⟩. ⟨hal-01652413⟩
Accès au bibtex
BibTex

Ouvrages

2021

ref_biblio
Mireille Blay-Fornarino, Catherine Dubois, Alain Giorgetti, Nikolai Kosmatov. Actes des journées du GDR GPL 2021. 2021. ⟨hal-03658364⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03658364/file/book-gdr-gpl-2021-fr.pdf BibTex

2015

ref_biblio
Catherine Dubois, Paolo Masci, Dominique Méry (Dir.). Second International Workshop on Formal Integrated Development Environment. EPTCS, 187, 2015, EPTCS ⟨10.4204/EPTCS.187⟩. ⟨hal-01246691⟩
Accès au bibtex
BibTex

2014

ref_biblio
David Delahaye, Catherine Dubois (Dir.). Proceedings of the first workshop about Sets and Tools, SETS 2014, affiliated to ABZ 2014. Informal proceedings. 2014. ⟨hal-01126518⟩
Accès au bibtex
BibTex
ref_biblio
Catherine Dubois, Régine Laleau. Actes de la 13 ème édition d'AFADL, atelier francophone sur les Approches Formelles dans l'Assistance au Développement de Logiciels, juin 2014.. Catherine Dubois, Régine Laleau. AFADL, pp.140, 2014. ⟨hal-00997676⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00997676/file/actes_AFADL2014.pdf BibTex
ref_biblio
Catherine Dubois, Dimitra Giannakopoulou, Dominique Méry (Dir.). Proceedings 1st Workshop on Formal Integrated Development Environment. Catherine Dubois; Dimitra Giannakopoulou; Dominique Méry. EPTCS, 149, pp.105, 2014, Electronic Proceedings in Theoretical Computer Science, ⟨10.4204/EPTCS.149⟩. ⟨hal-00987531⟩
Accès au bibtex
https://arxiv.org/pdf/1404.5785 BibTex
ref_biblio
Catherine Dubois, Laurence Duchien, Nicole Levy (Dir.). Actes des Sixièmes journées nationales du Groupement De Recherche CNRS du Génie de la Programmation et du Logiciel. Catherine Dubois; Laurence Duchien; Nicole Levy. Conservatoire National des Arts et Métiers, pp.239, 2014. ⟨hal-01055907⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01055907/file/201404_actes-gdr-gpl.pdf BibTex

2004

ref_biblio
Catherine Dubois, Valérie Ménissier-Morain. Apprentissage de la programmation avec OCaml. Hermès Sciences, 2004. ⟨hal-01520389⟩
Accès au bibtex
BibTex

Poster de conférence

2016

ref_biblio
Thi-Kim-Dung Pham, Catherine Dubois, Nicole Levy. Vers un développement formel non incrémental. AFADL 2016 : 15èmes journées des Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2016, Besançon, France. Edités par Aurélie Hurault et Nicolas Stouls, pp.106 - 113. ⟨hal-01677923⟩
Accès au bibtex
BibTex

Proceedings/Recueil des communications

2023

ref_biblio
Catherine Dubois, Manfred Kerber. Intelligent computer mathematics. Intelligent Computer Mathematics 16th International Conference (CICM ), 14101, Springer Nature Switzerland, 2023, Lecture Notes in Computer Science, 978-3-031-42752-7. ⟨10.1007/978-3-031-42753-4⟩. ⟨hal-04343372⟩
Accès au bibtex
BibTex
ref_biblio
Catherine Dubois, Pierluigi San Pietro. Formal methods teaching, 5th international workshop, FMTea 2023. 5th International Workshop (FMTea), 13962, Springer Nature Switzerland, 2023, Lecture Notes in Computer Science, ⟨10.1007/978-3-031-27534-0⟩. ⟨hal-04343457⟩
Accès au bibtex
BibTex

2022

ref_biblio
Catherine Dubois, Julien Cohen. STAF 2022 workshop proceedings: 10th international workshop on bidirectional transformations (BX 2022), 2nd international workshop on foundations and practice of visual modeling (FPVM 2022) and 2nd international workshop on MDE for smart IoT systems (MeSS 2022). Software Technologies: Applications and Foundations federation of conferences (STAF 2022), 3250, 2022. ⟨hal-04344127⟩
Accès au bibtex
BibTex

2021

ref_biblio
Catherine Dubois, Steffen Zschaler. 17 th educators symposium at MODELS 2021. 17th Educators Symposium at MODELS 2021, IEEE, 2021, ⟨10.1109/MODELS-C53483.2021.00112⟩. ⟨hal-04343448⟩
Accès au bibtex
BibTex

2018

ref_biblio
Catherine Dubois, Burkhart Wolff. Tests and proofs. International Conference on Tests and Proofs (TAP), 10889, Springer International Publishing, 2018, Lecture Notes in Computer Science, 978-3-319-92994-1. ⟨10.1007/978-3-319-92994-1⟩. ⟨hal-04489926⟩
Accès au bibtex
BibTex

2017

ref_biblio
Catherine Dubois, Bruno Woltzenlogel Paleo. Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving. Fifth Workshop on Proof Exchange for Theorem Proving (PxTP 2017), Electronic Proceedings in Theoretical Computer Science, 262, 2017, ⟨10.4204/EPTCS.262⟩. ⟨hal-04489940⟩
Accès au bibtex
https://arxiv.org/pdf/1712.00898 BibTex

Rapport

2017

ref_biblio
Gilles Dowek, Catherine Dubois, Brigitte Pientka, Florian Rabe. Universality of proofs. [Research Report] Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise; Services répartis, Architectures, MOdélisation, Validation, Administration des Réseaux (Institut Mines-Télécom-Télécom SudParis-CNRS); INRIA Saclay - Ile de France (INRIA); Jacobs University [Bremen]; École normale supérieure - Cachan; McGill University / Université McGill. 2017, pp.24. ⟨hal-01678845⟩
Accès au bibtex
BibTex

2006

ref_biblio
Marianne Simonot, Maria-Virginia Aponte, Catherine Dubois. État de l'art du typage pour l'intéropérabilité entre composants. [Research Report] CEDRIC-06-1182, CEDRIC Lab/CNAM. 2006. ⟨hal-01125296⟩
Accès au bibtex
BibTex

2004

ref_biblio
Stéphane Fechter, Catherine Dubois. Towards a formal definition of the Foc language. [Research Report] lip6.2004.001, LIP6. 2004. ⟨hal-02545623⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02545623/file/lip6.2004.001.pdf BibTex

Pré-publication, Document de travail

2021

ref_biblio
Mireille Blay-Fornarino, Catherine Dubois, Pierre-Etienne Moreau. GdR Génie de la Programmation et du Logiciel, Défis 2030. 2021. ⟨hal-03097727⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03097727/file/GDR_GPL_DEFIS_2030.pdf BibTex

2016

ref_biblio
Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, et al.. Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory. 2016. ⟨hal-04281492⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04281492/file/expressing.pdf BibTex

2015

ref_biblio
Raphaël Cauderlier, Catherine Dubois. Objects and subtyping in the λΠ-calculus modulo. 2015. ⟨hal-01097444v2⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01097444/file/article_types.pdf BibTex