Laboratoire Cédric

	Axe : Certification de preuves automatiques

Accueil

english version

Équipe CPR
Participants Pierre Courtieu, Maître de Conférences
Julien Forest, Maître de Conférences
Olivier Pons, Maître de Conférences
Xavier Urbain, Maître de Conférences

Présentation

Ce thème vise à la certification (par des outils de preuve mécanique, c'est-à-dire des assistants à la preuve) des résultats de démonstrateurs automatiques (sans interaction avec l'utilisateur) afin de permettre leur utilisation en conjonction avec des assistants à la preuve.

Actuellement les travaux de l'équipe se concentrent sur l'outil CiME et la production automatique de certificats Coq pour des preuves (CiME) de propriétés liées à la réécriture.
CiME3 traçant, c'est-à-dire produisant des traces vérifiables par Coq, et utilisant une partie du moteur de terminaison de CiME 2.04 est disponible ici .

Ces travaux prennent place au sein du projet ANR A3PAT .

[2010] [2009] [2008] [2007] [2006] [2005] [2004] [2003] [2002] [2001] [2000] [1999] [1998] [1997] [1996] [1995] [1994] [1993] [1992]

Publications 2010

[Revues internationales][Conférences internationales majeures][Conférences internationales][Revues nationales][Conférences nationales][Livres][Rapports de recherche][Chapitres de livres][Mémoires d'ingénieurs][Divers][Rapports d'Activités][Thèses]

Conférences internationales majeures

[CCF10] E. Contejean, P. Courtieu, J. Forest, A. Paskevich, O. Pons et X. Urbain. A3PAT, an Approach for Certified Automated Termination Proofs . In PEPM'10 Proceedings of the 2010 ACM SIGPLAN Symposium on Partial Evaluation and Program Manipulation, Madrid, Spain, January, pp. 10, ACM Press, 2010. To appear . (ref. CEDRIC 1833)

[CGP10] P. Courtieu, G. Gbedo et O. Pons. Improved Matrix Interpretation . In SOFSEM'10, Int. Conf. on Current Trends in Theory and Practice of Computer Science, ÂŠpindlerův MlÃ½n - RÃ©publique TchÃ¨que, Janvier, LNCS, pp. 12, Springer-Verlag, 2010. To appear . (ref. CEDRIC 1817)

Publications 2009

Conférences internationales

[CGP09] P. Courtieu, G. Gbedo et O. Pons. Matrix interpretations revisited . In Extended Abstracts of the 10th International Workshop on Termination, WST'09, Leipzig, Germany, Ju, pp. 4, A. Geser, 2009. (télécharger) (ref. CEDRIC 1710)

Publications 2008

Revues internationales

[DLM08] F. Duran, S. Lucas, J. Meseguer, C. Marché et X. Urbain. Proving Operational Termination of Membership Equational Programs . Higher Order and Symbolic Computation, 21(1): 59-88, 2008. (ref. CEDRIC 1111)

Conférences internationales majeures

[DÉV08] D. Delahaye, J.-F. Étienne et V. Viguié Donzeau-Gouge. A Formal and Sound Transformation from Focal to UML: An Application to Airport Security Regulations . In UML&FM'08 UML and Formal Methods, Kitakyushu-City (Japan), October, ISSE NASA Journal, Springer, 2008. (ref. CEDRIC 1630)

[DÉV08b] D. Delahaye, J.-F. Étienne et V. Viguié Donzeau-Gouge. Producing UML Models from Focal Specifications: An Application to Airport Security Regulations . In TASE'08 Theoretical Aspects of Software Engineering, Nanjing (China), June, IEEE CS Press, 2008. (ref. CEDRIC 1628)

[GLU08] R. Gutierrez, S. Lucas et X. Urbain. Usable Rules for Context-Sensitive Rewriting . In 19th Int. Conf. on Rewriting Techniques and Applications, Linz, Autriche, juin, LNCS 5117, pp. 126-141, 2008. (ref. CEDRIC 1548)

[CFU08] P. Courtieu, J. Forest et X. Urbain. Certifying a Termination Criterion Based on Graphs, without Graphs . In TPHOLs'08 Theorem Proving in Higher Order Logics, MontrÃ©al, Canada, aug, pp. 183-198, C. Munoz et O. Ait Mohamed, 2008. LNCS 5170. (ref. CEDRIC 1533)

Conférences internationales

[DÉV08c] D. Delahaye, J.-F. Étienne et V. Viguié Donzeau-Gouge. Formal Modeling of Airport Security Regulations using the Focal Environment . In RELAW'08 Requirements Engineering and Law, Barcelona (Spain), September, IEEE CS Press, 2008. (ref. CEDRIC 1629)

Rapports de recherche

[CFU08b] É. Contejean, J. Forest et X. Urbain. Deep-Embedded Unification . Rapport scientifique CEDRIC No 1547, 2008. (ref. CEDRIC 1547)

Communications par affiche dans un congrès national

[BAR08] F. Barthelemy. Typage, produit cartésien et unités d'analyse pour les modèles à états finis . Poster in TALN'08 Traitement Automatique des Langues, Avignon, juin, pp. 380-389, 2008. (télécharger) (ref. CEDRIC 1625)

Publications 2007

Conférences internationales majeures

[BAR07] F. Barthélemy. Using Mazurkiewicz Trace Languages for Partition-Based Morphology . In ACL'07 Annual Metteing of the Association for Computational Linguistics, 2007. (ref. CEDRIC 1374)

[JD07] É. Jaeger et C. Dubois:. Why Would You Trust B ? . In LPAR'07 Logic for Programming Artificial Intelligence and Reasoning, Yerevan (Armenia), October, LNCS 4790, pp. 288-302, Nachum Dershowitz, Andrei Voro, 2007. (ref. CEDRIC 1352)

[DDE07] D. Delahaye, C. Dubois et J.-F. Etienne. Extracting Purely Functional Contents from Logical Inductive Types . In TPHOLs'07 Theorem Proving in Higher Order Logics, Kaiserslautern (Germany), September, LNCS 4732, pp. 70-85, Klaus Schneider, Jens Brandt, 2007. (ref. CEDRIC 1284)

[CCF07] É. Contejean, P. Courtieu, J. Forest, O. Pons et X. Urbain. Certification of automated termination proofs . In 6th Int. Symp. on Frontiers of Combining Systems, Liverpool, Royaume-Uni, sept., LNAI 4720, pp. 148-162, Boris Konev et Frank Wolter, 2007. (ref. CEDRIC 1203)

[GFL07] F. Gervais, M. Frappier et R. Laleau. Refinement of EB3 Process Patterns into B Specifications . In B2007, BesanÃ§on, France, Janvier, LNCS 4355, pp. 201-215, 2007. (ref. CEDRIC 1119)

Conférences internationales

[BAR07b] F. Barthélemy. Finite-State Compilation of Feature Structures for Two-Level Morphology . In FSMNLP'07, Finite-State Methods and Natural Language Processing, Postsdam (Germany), 2007. (ref. CEDRIC 1376)

[BAR07c] F. Barthélemy. Multi-Grain Relations . In CIAA'07 Int. Conf. on Implementation and Application of Automata, Prague (Rep. TchÃ¨que), LNCS 4783, pp. 243-252, Jan Holub and Jan Ždárek, 2007. (ref. CEDRIC 1375)

[FFG07] M. Frappier, B. Fraikin, F. Gervais, R. Laleau et M. Richard. Synthesizing information systems: the APIS project . In RCIS'07 First Int. Conf. on Research Challenges in Information Science, Ouarzazate, pp. 73-84, 2007. (ref. CEDRIC 1192)

Conférences nationales

[BAR07d] F. Barthélemy. Cunéiforme et SMS: analyse graphémique de systèmes d'écriture hétérogènes . In Colloque Lexique et grammaire, Bonifacio (France), octobre, 2007. (ref. CEDRIC 1377)

[BAR07e] F. Barthélemy. Structures de traits typées et morphologie à partition . In TALN'07 Traitement Automatique des Langues, Toulouse, France, pp. 69-78, 2007. (ref. CEDRIC 1373)

[GLU07] R. Gutiérrez, S. Lucas et X. Urbain. Towards a notion of Usable Rule for Context-Sensitive Rewrite Systems . In PROLE'07 7th Spanish Conference on Programming and Computer Languages, Saragosse, Espagne, sept., Ernesto Pimentel, 2007. À paraître. (ref. CEDRIC 1278)

Rapports de recherche

[NG07] K. Nakata et J. Garrigue. Path resolution for recursive nested modules is undecidable . Rapport scientifique CEDRIC No 1202, 2007. (télécharger) (ref. CEDRIC 1202)

[CCF07b] E. Contejean, P. Courtieu, J. Forest, O. Pons et X. Urbain. Certification of automated termination proofs . Rapport scientifique CEDRIC No 1185, 2007. (télécharger) (ref. CEDRIC 1185)

Publications 2006

Conférences internationales majeures

[NPV06] E. Najm, J.-F. Pradat-Peyre et V. Viguié Donzeau-Gouge. FORTE'06: Formal Techniques for Networking and Distributed Systems . In , LNCS 4229, 2006. (ref. CEDRIC 1094)

Conférences internationales

[GBF06] F. Gervais, P. Batanado, M. Frappier et R. Laleau. EB3TG: A Tool Synthesizing Relational Database Transactions From EB3 Attribute Definitions . In ICEIS'06, Paphos, Chypre, May, ISAS, pp. 44-51, INSTICC, 2006. (ref. CEDRIC 979)

Conférences nationales

[BAR06] F. Barthélemy. Un analyseur morphologique multi-niveaux utilisant la jointure . In TALN'06 Traitement Automatique des Langues, Louvin, Belgique, 2006. (ref. CEDRIC 1491)

[MGL06] A. Mammar, F. Gervais et R. Laleau. Systematic Identification of Preconditions from Set-Based Integrity Constraints . In INFORSID'06, Hammamet, Tunisie, 1-3 Juin, pp. 595-610, 2006. (ref. CEDRIC 1009)

[GER06] F. Gervais. EB4 : Vers une méthode de spécification formelle des SI . In INFORSID'06, Hammamet, Tunisie, 1-3 Juin, pp. 561-576, 2006. (ref. CEDRIC 1008)

[BGF06] P. Batanado, F. Gervais, M. Frappier et R. Laleau. EB3TG : Un outil de génération de transactions de base de données relationnelle pour EB3 . In AFADL'06 - Approches Formelles dans l'Assistance au DÃ©veloppement de Logiciels, Paris, France. 200, 2006. (télécharger) (ref. CEDRIC 978)

[GBF06b] F. Gervais, P. Batanado, M. Frappier et R. Laleau. Génération automatique de transactions de base de données relationnelle à partir de définitions d'attributs EB3 . In AFADL'06 Approches Formelles dans l'Assistance au DÃ©veloppement de Logiciels, Paris, France, pp. 25-39, 2006. (télécharger) (ref. CEDRIC 977)

Rapports de recherche

[VS06] M. V. Aponte et M. Simonot. Spécification et vérification de composants : état de l'art . Rapport scientifique CEDRIC No 1180, 2006. (ref. CEDRIC 1180)

[GFL06] F. Gervais, M. Frappier et R. Laleau. Defining and Proving B Refinements for the Patterns of EB3 Process Expressions . Rapport scientifique CEDRIC No 996, 2006. (ref. CEDRIC 996)

Chapitres de livres

[GFS06] F. Gervais, M. Frappier et R. St-Denis. EB3 : Formal Language and Application . Chapitre de livre : "Software Specification Methods", ISBN 1-905209-34-7, pp. 259-274, ISTE, 2006. (ref. CEDRIC 980)

Thèses

[GER06b] F. Gervais. Combinaison de spécifications formelles pour la modélisation des systèmes d'information . Thèse CEDRIC, 2006. (télécharger) (ref. CEDRIC 1103)

Publications 2005

Revues internationales

[BCD05] G. Barthe, P. Courtieu, G. Dufay et S. Melo de Sousa. Tool-assisted specification and verification of Typed Low-Level Languages . JAR, J. of Automated Reasoning, 35(4): 295-354, 2005. (télécharger) (ref. CEDRIC 1718)

[CMP05] E. Contejean, C. Marché, A. Paula Tomas et X. Urbain. Mechanically proving termination using polynomial interpretations . JAR, J. of Automated Reasoning, 34(4): 325-363, 2005. (ref. CEDRIC 710)

Conférences internationales majeures

[GFL05] F. Gervais, M. Frappier et R. Laleau. Synthesizing B Specifications from EB3 Attribute Definitions . In IFM'05, Eindhoven, Pays-Bas, 29 Nov. - 2 DÃ©c., LNCS 3771, pp. 207-226, 2005. (c) Springer-Verlag. (ref. CEDRIC 840)

[GFL05b] F. Gervais, M. Frappier et R. Laleau. Generating Relational Database Transactions From Recursive Functions Defined on EB3 Traces . In SEFM'05, Coblence, Allemagne, 7-9 Septembre, pp. 117-126, 2005. (c) IEEE Computer Society Press. (ref. CEDRIC 830)

Conférences internationales

[LVL05] R. Laleau, S. Vignes, Y. Ledru, M. Lemoine, D. Bert, V. Donzeau-Gouge, C. Dubois et F. Peureux. Application of Requirements Engineering Techniques to the Analysis of Civil Aviation Security Standards . In SREP'05 International Workshop, In conjunction with 13th IEEE International Requirements Engineering, 2005. (ref. CEDRIC 905)

[BAR05] F. Barthélemy. Partitioning Multitape Transducers . In FSMNLP'05 Finite State Methods in Natural Language Processing, Helsinki, Finlande, sept, LNCS 4002, 2005. (ref. CEDRIC 887)

[GFL05c] F. Gervais, M. Frappier et R. Laleau. How to Synthesize Relational Database Transactions From EB3 Attribute Definitions? . In MSVVEIS'05, Miami, USA, May, pp. 83-88, INSTICC Press, 2005. (télécharger) (ref. CEDRIC 737)

Revues nationales

[DJP05] D. Delahaye, M. Jaume et V. Prevosto. Coq: un outil pour l'enseignement . TSI, Technique et Science Informatiques, 24(9): 1139-1160, Lavoisier, 2005. (ref. CEDRIC 878)

Rapports de recherche

[GFL05d] F. Gervais, M. Frappier et R. Laleau. Vous avez dit raffinement ? . Rapport scientifique CEDRIC No 829, 2005. (télécharger) (ref. CEDRIC 829)

[GFL05e] F. Gervais, M. Frappier, R. Laleau et P. Batanado. EB3 Attribute Definitions: Formal Language and Application . Rapport scientifique CEDRIC No 700, 2005. (télécharger) (ref. CEDRIC 700)

Thèses

[AMI05] P. Amiranoff. Une modélisation de l’analyse de programmes par instances à travers la théorie des automates : les transducteurs comme relation des instances aux emplacements mémoire . Thèse CEDRIC, 2005. (ref. CEDRIC 1494)

Publications 2004

Revues nationales

[BDF04] K. Berkani, C. Dubois, A. Faivre et J. Falampin. Validation des règles de base de l'Atelier B . TSI, Technique et Science Informatiques, 23(7): 855-878, 2004. (ref. CEDRIC 707)

Conférences nationales

[DJP04] C. Dubois, M. Jaume, O. Pons et V. Prevosto. L'atelier Focal . In AFADL, session outils, 2004. (ref. CEDRIC 837)

[ML04] A. Mammar et R. Laleau. UML2SQL: Un environment intégré pour le développement d'implémentations relationnelles à partir de diagrammes UML . In AFADL'04, 2004. (ref. CEDRIC 640)

[ML04b] A. Mammar et R. Laleau. Génération de code à partir d'une spécification B: application aux bases de données . In AFADL'04, 2004. (ref. CEDRIC 636)

Rapports de recherche

[GFL04] F. Gervais, M. Frappier et R. Laleau. Synthesizing B Substitutions for EB3 Attribute Definitions . Rapport scientifique CEDRIC No 683, 2004. (télécharger) (ref. CEDRIC 683)

[LM04] R. Laleau et A. Mammar. UML2SQL: An Integrated Environment for the Development of UML and SQL Specifications . Rapport scientifique CEDRIC No 643, 2004. (ref. CEDRIC 643)

Chapitres de livres

[DM04] C. Dubois et V. Ménissier-Morain. Apprentissage de la programmation avec OCaml . Chapitre de livre : "", Hermès Sciences, 2004. (ref. CEDRIC 719)

Divers

[GER04] F. Gervais. EB4 : Vers une méthode combinée de spécification formelle des systèmes d'information . Divers, 2004. Examen de spécialité, Doctorat Informatique, Université de Sherbrooke (Québec), Juin 2004.. (télécharger) (ref. CEDRIC 658)

Publications 2003

Conférences internationales majeures

[BGL03] S. Blazy, F. Gervais et R. Laleau. Reuse of Specification Patterns with the B Method . In ZB 2003: Formal Specification and Development in Z and B, Turku, Finland, 4-6 June 2003, LNCS 2651, pp. 40-57, Springer-Verlag, 2003. 3rd International Conference of B and Z Users.. (télécharger) (ref. CEDRIC 443)

Conférences internationales

[BFG03] C. Bigot, A. Faivre, J.P. Gallois, A. Lapitre, D. Lugato, J.Y. Pierron et N. Rapin. Automatic test generation with AGATHA, . In , LNCS 2619, pp. 591-596, 2003. (ref. CEDRIC 962)

[ML03] A. Mammar et R. Laleau. Design of an Automatic Prover Dedicated to the Refinement of Database Applications . In FM'2003, Springer-Verlag, LNCS nÂ° 2805, pp 834-854, Pise,Italy, Sept, 2003. . (télécharger) (ref. CEDRIC 346)

Conférences nationales

[BGL03b] S. Blazy, F. Gervais et R. Laleau. Une démarche outillée pour spécifier formellement des patrons de conception réutilisables . In Objets, Composants et ModÃ¨les dans l'ingÃ©nierie des SI, 2003. Workshop associé à INFORSID'2003, Nancy, 3 juin 2003.. (télécharger) (ref. CEDRIC 484)

[BDF03] K. Berkani, C. Dubois, A. Faivre et J. Falampin. Validation des règles de base de l'Atelier B . In AFADL'03, 2003. Rennes. (ref. CEDRIC 467)

Publications 2002

Conférences internationales majeures

[DEL02] D. Delahaye. Free-style Theorem Proving . In Proceedings of Theorem Proving in Higher Order Logics (TPHOLs), Hampton (VA, USA), LNCS 2410, pp. 164-181, Springer, LNCS (2410), 2002. (télécharger) (ref. CEDRIC 872)

Conférences internationales

[ACC02] M.V. Aponte, E. Chailloux, G. Cousineau et P. Manoury. Advanced programming features in objective caml. . In 6eme Brazilian Symposium on Programming Languages. -- Rio de Janeiro, 2002. (ref. CEDRIC 884)

[DEL02b] D. Delahaye. A Proof Dedicated Meta-Language . In Proceedings of Logical Frameworks and Meta-Languages (LFM), Copenhagen (Denmark), ENTCS 70, Elsevier, ENTCS (70-2), 2002. (télécharger) (ref. CEDRIC 871)

[LSV02] N. Lopez, M. Simonot et V. Viguié Donzeau-Gouge. A methodological process for the design of a large system: two industrial case-studies. . In Formal Methods for Industrial Critical Systems (FMICS'02), Elsevier Science B.V., 2002. (télécharger) (ref. CEDRIC 446)

[ABD02] M. Aiguier, D. Bahrami et C. Dubois. On a Generalised Logicality Theorem . In , 2002. LNAI 2385. (ref. CEDRIC 425)

[FFL02] M. Frappier, B. Fraikin, R. Laleau et M. Richard. APIS : Automatic Production of Information Systems . In International AAAI 2002 Spring Symposium : Logic-Based Program Synthesis: State-of-the-Art and Futur, 2002. (ref. CEDRIC 423)

[LP02] R. Laleau et F. Polack. Coming and going from UML to B : a proposal to support traceability in rigorous IS development . In ZB?2002: Int. Conf. on Formal Specification and Development in Z and B, LNCS de Springer-Verlag, 2002. Grenoble, France, Janvier 2002. (télécharger) (ref. CEDRIC 393)

Revues nationales

[BOI02] O. Boite. Automatiser les preuves d'un sous-langage de la méthode B . TSI, Technique et Science Informatiques, 20(8), 2002. (ref. CEDRIC 428)

Rapports de recherche

[FB02] S. Fechter et O. Boite. BBFoc . Rapport scientifique CEDRIC No 685, pp. 19, 2002. (télécharger) (ref. CEDRIC 685)

[BLA02] S. Blazy. Transformations certifiées de programmes impératifs . Rapport scientifique CEDRIC No 398, 2002. (ref. CEDRIC 398)

[BGL02] S. Blazy, F. Gervais et R. Laleau. Un exemple de réutilisation de patterns de spécification avec la méthode B . Rapport scientifique CEDRIC No 395, 2002. (télécharger) (ref. CEDRIC 395)

Divers

[GER02] F. Gervais. Réutilisation de composants de spécification en B . Divers, 2002. Rapport de stage, DEA Informatique, Université d'Evry, Juillet 2002.. (télécharger) (ref. CEDRIC 394)

Thèses

[MAM02] A. Mammar. Un environnement formel pour le développement d'applications bases de données . Thèse CEDRIC, 2002. (télécharger) (ref. CEDRIC 392)

[LOP02] N. Lopez. Spécification de systèmes complexes: méthodes et techniques . Thèse CEDRIC, 2002. (télécharger) (ref. CEDRIC 322)

Habilitation à Diriger la Recherche

[LAL02] R. Laleau. Conception et développement formels d'applications bases de données . Habilitation à Diriger la recherche CEDRIC (HDR), 2002. Habilitation à diriger des recherches, Université d'Evry, décembre 2002. (télécharger) (ref. CEDRIC 424)

Publications 2001

Revues internationales

[MS01] F. Monin et M. Simonot. An ordinal measure based procedure for termination of functions . Theoretical computer Science, 254(0), 2001. (ref. CEDRIC 1077)

[LP01] R. Laleau et F. Polack. Specification of integrity-preserving operations in information systems by using a formal UML-based language . Information and Software Technology, 2001. Elsevier, M. Dyer and M. Shepperd eds, article accepté. (télécharger) (ref. CEDRIC 275)

Conférences internationales

[LM01] R. Laleau et A. Mammar. An Automatic Generation of B Specifications from Well-defined UML Notations for Database Applications . In Int. Symp. on Programming Systems, Alger, AlgÃ©rie, Mai, 2001. (télécharger) (ref. CEDRIC 274)

[LP01b] R. Laleau et F. Polack. A Rigorous Metamodel for UML Static Conceptual Modelling of Information Systems Specification . In CAISE'01, Interlaken, Suisse, Juin, 2001. Volume LNCS 2068, Springer-Verlag. (télécharger) (ref. CEDRIC 273)

Conférences nationales

[DM01] D. Delahaye et M. Mayero. Field: une procédure de décision pour les nombres réels en Coq . In JournÃ©es Francophones des Langages Applicatifs (JFLA), Pontarlier (France), INRIA, 2001. (télécharger) (ref. CEDRIC 869)

[MAM01] A. Mammar. Une approche formelle par raffinement pour le développement d'applications bases de données sûres . In 19Ã¨me congrÃ©s INFORSID, GenÃ¨ve, Suisse, 2001. article sélectionné pour un numéro spécial de la revue ISI-TSI. (ref. CEDRIC 278)

[BOI01] O. Boite. Prouveur Spécialisé pour le Langage d'Ensembles d'Entiers et de Booléens : LEEB . In AFADL'01, 2001. (ref. CEDRIC 266)

Rapports de recherche

[LM01b] R. Laleau et A. Mammar. Réutilisation des preuves dans le processus de raffinement B . Rapport scientifique CEDRIC No 377, 2001. (ref. CEDRIC 377)

[LM01c] R. Laleau et A. Mammar. Un exemple de génération d'une implémentation relationnelle à partir d'une spécification B . Rapport scientifique CEDRIC No 368, 2001. (ref. CEDRIC 368)

[FL01] M. Frappier et R. Laleau. Proving the Refinement of Scenarios into Object-Oriented Models . Rapport scientifique CEDRIC No 277, 2001. , rapport technique n°272 du DMI, Université de Sherbrooke, Quebec . (télécharger) (ref. CEDRIC 277)

[LL01] N. Lammari et R. Laleau. Complementary Mechanisms Based on Applicability Constraints for Supporting IS-A Inheritance Hierarchies Design . Rapport scientifique CEDRIC No 276, 2001. (ref. CEDRIC 276)

Thèses

[DEL01] D. Delahaye. Conception de langages pour décrire les preuves et les automatisations dans les outils d'aide à la preuve: une étude dans le cadre du système Coq . Thèse CEDRIC, 2001. (télécharger) (ref. CEDRIC 870)

Publications 2000

Revues internationales

[BLA00] S. Blazy. Specifying and Automatically Generating a Specialization Tool for Fortran 90 . Journal on Automated Software Engineerin, 7(4): 345-376, Kluwer academic publishers, 2000. (ref. CEDRIC 284)

Conférences internationales majeures

[DEL00] D. Delahaye. A Tactic Language for the System Coq . In Proceedings of Logic for Programming and Automated Reasoning (LPAR), Reunion Island (France), LNCS/LNAI 1955, pp. 85-95, Springer, LNCS/LNAI (1955), 2000. (télécharger) (ref. CEDRIC 867)

Conférences internationales

[BBM00] S. Bocs, S. Blazy, C. Médigue et P. Glaser. An automatic detection of prokaryotic CoDing Sequences Combining Several Independent Methods . In Genome 2000, Paris, 11-15 avril 2000, 2000. (ref. CEDRIC 283)

[ABD00] M. Aiguier, D. Bahrami et C. Dubois. Axioms for Rewriting Theory . In PLI 2000, Workshop RULE 2000 : First International Workshop on Rule-Based Programming Montreal, Cana, 2000. (ref. CEDRIC 230)

[LM00] R. Laleau et A. Mammar. A Generic Process to Refine a B Specification into a Relational Database Implementation . In First Int. Conf. of B and Z users (ZB2000), Springer-Verlag, LNCS nÂ° 1878, York, UK, Aout/Sept., 2000. (télécharger) (ref. CEDRIC 104)

[LP00] R. Laleau et F. Polack. Metamodels for Static Conceptual Modelling of Information Systems . In Workshop on Defining Precise Semantics for UML, ECOOP'2000, Sophia Antipolis, France, June, 2000. (ref. CEDRIC 92)

[LM00b] R. Laleau et A. Mammar. An Overview of a Method and its support Tool for Generating B Specifications from UML Notations . In 15th IEEE Int. Conf. on Automated Software Engineering (ASE2000), Grenoble, France, Septembre, 2000. (ref. CEDRIC 89)

[LAL00] R. Laleau. On the Interest of Combining UML with the B Formal Method for the Specification of Database Applications . In Int. Conf. on Enterprise Information Systems (ICEIS 2000), Stafford, UK, July, 2000. (ref. CEDRIC 88)

[LSV00] N. Lopez, M. Simonot et V. Viguie Donzeau-Gouge. Deriving Software Specifications from Event Based Models . In ZB 2000, Int. Conf.rence of B and Z Users, 29aug-2sept 2000, York, U.K., 2000. (ref. CEDRIC 42)

Rapports de recherche

[LM00c] R. Laleau et A. Mammar. Using a Formal Refinement to Derive Relational Database Implementations from B Specifications . Rapport scientifique CEDRIC No 86, 2000. , extended version of the ZB2000 paper.. (ref. CEDRIC 86)

Chapitres de livres

[FLP00] P. Facon, R. Laleau et H. Phuong Nguyen. From OMT Diagrams to B Specifications . Chapitre de livre : "", 2000. "Software Specification Methods : an Overview Using a Case Study", Springer, FACIT series, eds : Marc Frappier and Henri Habrias, October 2000.. (ref. CEDRIC 93)

Thèses

[BUR00] L. Burdy. Traitement des expressions dépourvues de sens de la théorie des ensembles: Application à la méthode B . Thèse CEDRIC, 2000. (ref. CEDRIC 43)

Habilitation à Diriger la Recherche

[DUB00] C. Dubois. Un parcours de la programmation à la preuve . Habilitation à Diriger la recherche CEDRIC (HDR), 2000. Habilitation à diriger des recherches, Université d'Evry. (ref. CEDRIC 177)

Publications 1999

Conférences internationales majeures

[DEL99] D. Delahaye. Information Retrieval in a Coq Proof Library using Type Isomorphisms . In , pp. 131-147, Springer-Verlag, LNCS (1956), 1999. (télécharger) (ref. CEDRIC 732)

Revues nationales

[LLJ99] N. Lammari, R. Laleau et M. Jouve. Processus d'optimisation conceptuelle d'un schéma orienté-objet . L'Objet, 5(1), Hermes, 1999. (ref. CEDRIC 94)

Rapports de recherche

[FLM99] P. Facon, R. Laleau, A. Mammar et F. Polack. Formal Specification of the UML Metamodel for Building Rigorous Caise Tools . Rapport scientifique CEDRIC No 91, 1999. (ref. CEDRIC 91)

[FLM99b] P. Facon, R. Laleau et A. Mammar. Combining UML with the B Formal Method for the Specification of Database Applications . Rapport scientifique CEDRIC No 87, 1999. (ref. CEDRIC 87)

Publications 1998

Revues internationales

[BF98] S. Blazy et P. Facon. Partial evaluation for program comprehension . Symposium on Partial Evaluation, sept, 30(3), ACM Computing Surveys, 1998. (ref. CEDRIC 20)

Rapports de recherche

[SIM98] M. Simonot. Le raffinement algorithmique : définition par le haut et par le bas . Rapport scientifique CEDRIC No 1078, 1998. (ref. CEDRIC 1078)

Publications 1997

Conférences internationales

[BF97] S. Blazy et P. Facon. Application of formal methods to the development of a software maintenance tool . In IEEE Conf. on Automated Software Engineering, Lake Tahoe, 3-5 November, pp. 162-171, 1997. (ref. CEDRIC 22)

Conférences nationales

[DDW97] D. Delahaye, R. Di Cosmo et B. Werner. Recherche dans une bibliothèque de preuves Coq en utilisant le type et modulo isomorphismes . In PRC/GDR de programmation, PÃ´le Preuves et SpÃ©cifications AlgÃ©briques, 1997. (télécharger) (ref. CEDRIC 731)

Rapports de recherche

[DEL97] D. Delahaye. Search2: un outil de recherche dans une bibliothèque de preuves Coq modulo isomorphismes . Rapport scientifique CEDRIC No 730, 1997. Rapport du DEA Sémantique, Preuves et Programmation, Université Pierre et Marie Curie (Paris 6).. (télécharger) (ref. CEDRIC 730)

Publications 1996

Conférences internationales

[VD96] M. Virginia Aponte et R. Dicosmo. Type isomorphisms for module signatures . In Symposium on Programming Language Implementation and Logic Programming (PLILP), LNCS, pp. 334-346, Springer-Verlag, 1996. (ref. CEDRIC 882)

[BF96] S. Blazy et P. Facon. An automatic interprocedural analysis for the understanding of scientific application programs . In Seminar on partial evaluation, Dagsthul castle, 12-16 February, LNCS 1110, pp. 1-16, Springer-Verlag, 1996. (ref. CEDRIC 24)

[BF96b] S. Blazy et P. Facon. Interprocedural analysis for program comprehension by specialization . In 4th IEEE Workshop on Program Comprehension, Berlin, 29-31 March, pp. 133-141, IEEE, 1996. (ref. CEDRIC 23)

Conférences nationales

[AC96] M.-V. Aponte et G. Castagna. Programmation modulaire avec surcharge et liaison tardive . In JournÃ©es Francophones des Langages Applicatifs., INRIA, 1996. (ref. CEDRIC 883)

Publications 1995

Conférences internationales

[BF95] S. Blazy et P. Facon. Formal specification and prorotyping of a program specializer . In TAPSOFT'95, Aarhus, 22-26 May, LNCS 915, pp. 666-680, Springer-Verlag, 1995. (ref. CEDRIC 25)

Publications 1994

Revues internationales

[MS94] P. Manoury et M. Simonot. Automatizing termination proofs of recursively defined functions . Theoretical Computer Science, 135(0), 1994. (ref. CEDRIC 1075)

[BF94] S. Blazy et P. Facon. Partial evaluation for the understanding of Fortran programs . IJSEKE, Int. J. of Software Engineering and Knowledge Engineering, 4(4): 535-559, 1994. December 1994, International Journal of Software Engineering and Knowledge Engineering. (ref. CEDRIC 27)

Conférences internationales

[AL94] M.-V. Aponte et X. Leroy. Llamado de procedimientos a distancia y abstraccion de tipos . In Actes du 20e congres latino-americain d'informatique CLEI-PANEL, 1994. (ref. CEDRIC 881)

[BF94b] S. Blazy et P. Facon. SFAC: a tool for program comprehension by specialization . In 3rd IEEE Workshop on Program Comprehension, Washington D.C., 14-15 December, pp. 162-167, IEEE, 1994. (ref. CEDRIC 26)

Publications 1993

Conférences internationales

[MS93] P. Manoury et M. Simonot. A programming language with proofs . In Logic Programming and automated reasonning, LNCS 624, 1993. (ref. CEDRIC 1076)

[VIR93] M. Virginia Aponte. Extending Record typing to type parametric modules with sharing . In Tweentieth Annual Symposium on Principles of Programming Languages, Springer-Verlag, 1993. (ref. CEDRIC 879)

[BF93] S. Blazy et P. Facon. Partial evaluation and symbolic computation for the understanding of Fortran programs . In CAISE'93, Paris, France, June, LNCS 685, pp. 184-198, Springer Verlag, 1993. (ref. CEDRIC 30)

[BF93b] S. Blazy et P. Facon. Partial evaluation for the understanding of Fortran programs . In Soft. Eng. and Knowledge Eng. (SEKE), San Francisco, June, pp. 517-525, 1993. (ref. CEDRIC 29)

[BF93c] S. Blazy et P. Facon. Partial evaluation as an aid to the comprehension of Fortran programs . In 2nd IEEE Workshop on Program Comprehension, Capri, Italy, July, pp. 46-54, IEEE, 1993. (ref. CEDRIC 28)

Équipe	CPR
Participants	Pierre Courtieu, Maître de Conférences Julien Forest, Maître de Conférences Olivier Pons, Maître de Conférences Xavier Urbain, Maître de Conférences