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://hal.insa-toulouse.fr/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://hal.insa-toulouse.fr/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√©riÔ¨Ācation d‚Äôun environnement intelligent √† partir de sp√©ciÔ¨Ācations 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√©riÔ¨Ācation 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
Vincent Botbol, Ghiles Ziat, 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. ⟨hal-04551862⟩
Accès au bibtex
https://arxiv.org/pdf/2208.12747 BibTex
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

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://hal.insa-toulouse.fr/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. 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
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
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, 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
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

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: 12th International Conference, TAP 2018, Held as Part of STAF 2018, Toulouse, France, June 27-29, 2018, Proceedings. 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