CPR

Séminaire CPR

Présentation générale

Les travaux de l’équipe CPR s'inscrivent dans le développement et l'utilisation de méthodes formelles pour le développement de logiciels sûrs. Sûrs signifie ici que les logiciels développés vérifient les propriétés que l'on a énoncées formellement. Ces propriétés caractérisent les fonctionnalités du logiciel, mais peuvent aussi être relatives à la sûreté et la sécurité.

Nos travaux portent sur le développement de langages, théories, techniques de preuve pour la spécification, la conception, la programmation, et la vérification des logiciels (soit toute l'étendue du cycle de vie du logiciel).

Les axes majeurs de l'équipe CPR :

• Développement de l'atelier Focalize (anciennement Foc, puis Focal) - en collaboration avec l'équipe SPI (LIP6) et INRIA

  Focal permet de construire incrémentalement des composants de bibliothèque et prouver leur correction. Un composant, appelé espèce, peut contenir des énoncés de propriétés spécifiant le composant, des définitions de ses opérations et les preuves que ces opérations satisfont leurs spécifications.
  Les contributions principales de CPR : définition de la sémantique formelle du langage, traduction de Focal vers UMl, test de propriétés
  Applications : mathématiques effectives, sûreté dans les aéroports (projet EDEMOI)

• Certification d'outils

• Preuve automatique certifiée
  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 (dont la version 3 est en cours de développement) 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 déjà disponible à l'adresse http://a3pat.ensiie.fr/ .
• Vérification formelle de compilateurs Ce thème, développé en collaboration avec Xavier Leroy de l'INRIA, vise à produire un compilateur pour un sous-ensemble réaliste de C, entièrement vérifié à l'aide du système Coq. Nos contributions principales (travail de S. Blazy) concernent la vérification du front-end du compilateur et la formalisation d'un modèle mémoire pour C utilisé tout au long de la chaîne de compilation par les nombreux langages intermédiaires du compilateur. En collaboration avec l'équipe OC, nous étudions et formalisons également l'allocation de registres.
• Certification de générateurs aléatoires
  Ces travaux s'intéressent à la certification d'outils basés sur des générateurs aléatoires, avec pour cas d'étude un algorithme de tatouage contraint de base de données.
• Modélisation géométrique
  L’objectif est ici d’étudier l’application des méthodes formelles pour des applications de modélisation géométrique. Nous nous plaçons dans le cadre des modèles topologiques des cartes généralisées (G-cartes).

• Modélisation de composants logiciels

  Nous nous intéressons à la définition d'un modèle formel de composants, suffisameent général pour capturer la majorité des modèles existants. Nous avons défini un un modèle formel pour les composants à la Fractal capturant les aspects relatifs au contrôle des liaisons et à la reconfiguration dynamique. Le cadre proposé, nommé FracL, est fondé sur une description axiomatique des primitives de Fractal en logique de premier ordre, et permet la spécification et la preuve des propriétés autant fonctionnelles que de contrôle dans ces systèmes.

Projets récents

• Projets terminés récemment

  • A3PAT(2006 - juin 2009)
  • CerPAN (2006 - juin 2009)
  • Reve, 2006 - juin 2009
  • Compcert 2006 - juin 2009

• Projets en cours

  • SSURF (2007- juin 2010) (ANR SETIN)
  • Galapagos (2008-2010)
  • Scalp (2008-2011);
  • U3CAT (ANR Arpege, 2009-2011);
  • projet ÎdF-Digitéo PACTOLE

Publications 2010

Revues internationales

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)

Conférences internationales

Conférences nationales

[DDT10]

D. Delahaye, C. Dubois et P.-N. Tollitte. Génération de code fonctionnel certifié à partir de spécifications inductives dans l'environnement Focalize . In JFLA'10, Journées Francophones des Langages Applicatifs, La Ciotat, 2010. (ref. CEDRIC 1844)

Publications 2009

Revues internationales

Conférences internationales majeures

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)

[NR09]

I. Noyer et R. Rioboo. Reusing Proofs in a Mathematical Library . In Calculemus 2009, 2009. à paraitre. (ref. CEDRIC 1706)

Conférences nationales

[CDH09]

M. Carlier, C. Dubois, L. Habib et M. Jaume. Politique de contrôle d'accès multi-niveaux : test de conformité vis à vis des flots avec l'outil FoCaL . In AFADL'09 Approches formelles dans l'assistance au développement des Logiciels, Toulouse, janvier, IRIT Press, 2009. (ref. CEDRIC 1686)

Rapports de recherche

[CDG09]

M. Carlier, C. Dubois et A. Gotlieb. Constraint Reasoning in FocalTest . Rapport scientifique CEDRIC No 1703, pp. 36, 2009. (télécharger) (ref. CEDRIC 1703)

Thèses

Directions d'ouvrages ou de revues

Conférences données à l’invitation du Comité d’organisation dans un congrès national ou international

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É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

[CD08]

M. Carlier. Un Ancien et C. Dubois. Functional Testing in the Focal environment . In , LNCS 4966, pp. 84-98, Springer, 2008. (télécharger) (ref. CEDRIC 1369)

Revues nationales

Conférences nationales

[RIO08]

R. Rioboo. Concevoir et organiser une librairie de mathématiques effectives . In Journées Francophones des Langages applicatifs, 2008. (ref. CEDRIC 1704)

[BRS08]

S. Blazy, B. Robillard et E. Soutif. Coloration avec préférences : complexité, inégalités valides et vérification formelle . In ROADEF'08, Clermont-Ferrand, 25-27 Février, pp. 123-138, 2008. (ref. CEDRIC 1365)

[BRS08b]

S. Blazy, B. Robillard et E. Soutif. Vérification formelle d'un algorithme d'allocation de registres par coloration de graphe . In JFLA'08 Journées Francophones des Langages Applicatifs, pp. 31-46, INRIA, 2008. (ref. CEDRIC 1360)

Rapports de recherche

[BR08]

S. Blazy et B. Robillard. Live-Range Unsplitting for Faster Optimal Coalescing (extended version) . Rapport scientifique CEDRIC No 1609, 2008. (télécharger) (ref. CEDRIC 1609)

[AS08]

V. Aponte et M. Simonot. Une approche formelle de la reconfiguration dynamique . Rapport scientifique CEDRIC No 1590, pp. 27, 2008. (télécharger) (ref. CEDRIC 1590)

[AP08]

I. Augé et O. Pons. A service oriented compiler for operating systems . Rapport scientifique CEDRIC No 1551, 2008. (télécharger) (ref. CEDRIC 1551)

[ALP08]

I. Augé, V. Leligeour et O. Pons. A Distribution and System Compiler for Handling Heterogeneous Computer Site . Rapport scientifique CEDRIC No 1549, 2008. (télécharger) (ref. CEDRIC 1549)

[CFU08b]

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

Thèses

Habilitation à Diriger la Recherche

Directions d'ouvrages ou de revues

Communications par affiche dans un congrès national

Publications 2007

Revues internationales

Conférences internationales majeures

[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)

[BDD07]

R. Bonichon, D. Delahaye et D. Doligez. Zenon: an Extensible Automated Theorem Prover Producing Checkable Proofs . In LPAR'07 Logic for Programming Artificial Intelligence and Reasoning, Yerevan (Armenia), October, LNAI, pp. 151-165, 2007. (ref. CEDRIC 1285)

[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)

[WB07]

A. W. Appel et S. Blazy. Separation Logic for Small-step Cminor . In TPHOLs'07 Theorem Proving in Higher Order Logics, Kaiserslautern (Germany), September, LNCS 4732, pp. 5-21, Springer Verlag, 2007. (télécharger) (ref. CEDRIC 1210)

[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

[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)

[BLA07]

S. Blazy. Experiments in validating formal semantics for C . In C/C++ Verification Workshop, Oxford, United Kingdom, 2 July 2007, ICIS-R07015, pp. 95-102, Raboud University Nijmegen report, 2007. (télécharger) (ref. CEDRIC 1201)

[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)

Revues nationales

[MD07]

J. Marc Mota et C. Dubois. Raffinement de modèles topologiques : des droites aux 2-G-cartes . TSI, Technique et Science Informatiques, 26(7): 883-908, 2007. (ref. CEDRIC 1353)

Conférences nationales

[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)

[BRS07]

S. Blazy, B. Robillard et E. Soutif. Coloration avec préférences dans les graphes triangulés . In Journées Graphes et Algorithmes, Paris, 8-9 Novembre, pp. 32, 2007. (ref. CEDRIC 1368)

[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

[AB07]

A. Appel et S. Blazy. Separation logic for small-step Cminor (extended version) . Rapport scientifique CEDRIC No 1358, pp. 29 pages, INRIA, 2007. (ref. CEDRIC 1358)

[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)

Mémoires d'ingénieurs

Conférences données à l’invitation du Comité d’organisation dans un congrès national ou international

Publications 2006

Revues internationales

Conférences internationales majeures

[DEV06b]

D. Delahaye, J.-F. Etienne et V. Viguié Donzeau-Gouge. Certifying Airport Security Regulations using the Focal Environment . In FM'06: 14th Symposium on Formal Methods, Hamilton, Canada, August, LNCS 4085, pp. 48-63, 2006. (ref. CEDRIC 1282)

[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)

[BLD06]

S. Blazy, X. Leroy et Z. Dargaye. Formal verification of a C compiler front-end . In FM'06: 14th Symposium on Formal Methods, Hamilton, Canada, August, LNCS 4085, pp. 460-475, Springer-Verlag, 2006. (télécharger) (ref. CEDRIC 1027)

Conférences internationales

[LLL06]

Y. Ledru, R. Laleau, M. Lemoine, S. Vignes, D. Bert, V. Donzeau-Gouge, C. Dubois et F. Peureux. An attempt to combine UML and formal methods to model airport security . In CAISEÂ’06 Forum, 2006. (ref. CEDRIC 1098)

[DM06]

C. Dubois et J.-M. Mota. A formally verified geometric modelling core . In SERP'06 - Int. Conf. on Software Engineering Research and Practice, Las Vegas, USA,, CSREA Press, pp. 643-649, 2006. (ref. CEDRIC 1095)

[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

[MD06]

J.-M. Mota et C. Dubois. Raffinement de données en B événementiel pour les algorithmes géométriques . In AFADL'06 - Approches Formelles dans l'Assistance au Développement de Logiciels, Paris, France. 200, 2006. (ref. CEDRIC 1096)

[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

Thèses

Publications 2005

Revues internationales

[DM05]

D. Delahaye et M. Mayero. Dealing with Algebraic Expressions over a Field in Coq using Maple . JSC'05 J. of Symbolic Computation, 39(5): 569-592, Elsevier, 2005. (ref. CEDRIC 876)

[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

[BL05]

S. Blazy et X. Leroy. Formal verification of a memory model for C-like imperative languages . In ICFEM'05, Int. Conf on Formal Engineering Methods, Manchester, UK, 1-4 novembre 2005, LNCS 3785, pp. 280-299, Springer Verlag, 2005. (télécharger) (ref. CEDRIC 854)

[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

[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)

[VLN05]

M. Virginia Aponte, Y. Lyhyaoui et S. Natkin. Game Analysis of attacks on Online Games . In CGAIMS'05, Louisville, Kentucky, USA, july, 2005. (ref. CEDRIC 860)

[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

[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

[BIG05]

C. Bigot. Une proposition de formalisme orienté composant, application de méthodes d’exécution symbolique pour la validation de systèmes à base de composants . Thèse CEDRIC, 2005. (ref. CEDRIC 1493)

[BOI05]

O. Boite. Une aide à la réutilisation de preuves formelles - Application aux preuves de propriétés sémantiques . Thèse CEDRIC, pp. 160, 2005. (télécharger) (ref. CEDRIC 922)

Publications 2004

Conférences internationales majeures

[BOI04]

O. Boite. Proof Reuse with Extended Inductive Types . In TPHOLs 2004, LNCS 3223, pp. 50-65, K Slind et al., 2004. (ref. CEDRIC 686)

Conférences internationales

Revues nationales

Conférences nationales

[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

[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

Divers

Publications 2003

Revues internationales

Conférences internationales majeures

Conférences internationales

[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

[DGJ03]

C. Dubois, J. Grandguillot et M. Jaume. Réutilisation de preuves - Une étude pour le système Foc . In Journées francophones des langages applicatifs, 2003. Chamrousse. (ref. CEDRIC 468)

[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

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

[LMA02]

F. Ledoux, J.-M. Mota, A. Arnoult, C. Dubois, P. Le Gall, Y. Bertrand et . Spécifications formelles du chanfreinage . TSI, Technique et Science Informatiques, 21(8), 2002. 1073 - 1098. (ref. CEDRIC 426)

Rapports de recherche

[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

Thèses

[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

Publications 2001

Revues internationales

[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 majeures

Conférences internationales

[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

[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)

[LMA01]

F. Ledoux, J.-M. Mota, A. Arnould, C. Dubois, P. Le Gall et B. . Spécifications formelles du chanfreinage . In AFADL2001, 2001. Nancy. (ref. CEDRIC 231)

Rapports de recherche

[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

Publications 2000

Revues internationales

Conférences internationales majeures

Conférences internationales

[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

Chapitres de livres

Thèses

Habilitation à Diriger la Recherche

Publications 1999

Conférences internationales majeures

Revues nationales

Rapports de recherche

[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

Rapports de recherche

Publications 1997

Conférences internationales

Conférences nationales

Rapports de recherche

Publications 1996

Conférences internationales

[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

Publications 1995

Conférences internationales

Publications 1994

Revues internationales

[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

[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

[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)

Conférences nationales

Publications 1992

Conférences internationales

[HVM92]

M. Haziza, J.-F. Voidrot, E. Minor, L. Pofelski et S. Blazy. Software maintenance: an analysis of industrial needs and constraints . In IEEE Conf. on Software Maintenance, Orlando, 9-12 November, pp. 18-26, IEEE, 1992. (ref. CEDRIC 31)

Thèses