Publications Proposition GECCOO (2003)

[1] Alessandro Armando, Sylvio Ranise, and Michaël Rusinowitch. A rewriting approach to satisfiability procedures. Information and Computation, 2002. À paraître. [ bib ]
[2] F. Badeau, D. Bert, S. Boulmé, M-L. Potet, N. Stouls, and L. Voisin. Traduction de B vers des langages de programmation : points de vue du projet BOM. In Actes des Journées AFADL, IRISA, RENNES, Janvier 2003. [ bib ]
[3] Hector Ruiz Barradas and Didier Bert. Specification and Proof of Liveness Properties under Fairness Assumptions in B Event Systems. In Integrated Formal Methods, IFM2002, volume 2335 of LNCS, pages 360-379. Springer-Verlag, May 2002. [ bib ]
[4] F. Bellegarde, C. Darlotand J. Julliand, and O. Kouchnarenko. Reformulation : a Way to Combine Dynamic Properties and B Refinement. In FME 2001 (Formal Methods Europe), volume 2021 of LNCS. Springer-Verlag, 2001. [ bib ]
[5] F. Bellegarde, J. Julliand, and O. Kouchnarenko. Ready-simulation is not Ready to Express a Modular Refinement Relation. In Fundamental Aspects of Software Engineering 2000, FASE'2000, volume 1783 of LNCS. Springer-Verlag, 2000. [ bib ]
[6] F. Bellegarde, J. Julliand, and O. Kouchnarenko. Synchronized Parallel Composition of Event Systems in B. In 2nd International Conference of B and Z Users, ZB2002, volume 2272 of LNCS. Springer-Verlag, 2002. [ bib ]
[7] Didier Bert. Preuve de propriétés d'équité en B : étude du protocole du bus SCSI-3. In J. Souquières, editor, Actes de l'Atelier AFADL'2001, pages 221-241, LORIA, Nancy, France, June 2001. [ bib ]
[8] Didier Bert. Spécification algébrique et prototypage du << contrôle d'accès >> en LPG. Technique et Science Informatiques, 20(7):849-873, 2001. [ bib ]
[9] Didier Bert and Francis Cave. Construction of Finite Labelled Transition Systems from B Abstract Systems. In Integrated Formal Methods, IFM2000, volume 1945 of LNCS, pages 235-254. Springer-Verlag, November 2000. [ bib ]
[10] Didier Bert, Marie-Laure Potet, and Yann Rouzaud. A study on components and assembly primitives in B. In H. Habrias, editor, Proc. of First B Conference, Novembre 1996. [ bib ]
[11] Sylvain Boulmé. Opérateurs de raffinement sur les structures algébriques. In Journées Francophones des Langages Applicatifs. INRIA, February 2000. [ bib ]
[12] Sylvain Boulmé. Spécification d'un environnement dédié à la programmation certifiée de bibliothèques de calcul formel. PhD thesis, Université Paris 6, December 2000. [ bib ]
[13] Sylvain Boulmé. Interprétation de programmes orientés objet annotés en théorie des types. Etude préliminaire, non publiée, December 2002. [ bib ]
[14] Sylvain Boulmé. Toward a High Order Functional and Imperative Specification Language. Unpublished, February 2003. [ bib ]
[15] Sylvain Boulmé and Grégoire Hamon. Certifying synchrony for free. LNCS, 2250, 2001. [ bib ]
[16] Sylvain Boulmé, Thérèse Hardin, and Renaud Rioboo. Modules, objets et calcul formel. In Journées Francophones des Langages Applicatifs. INRIA, February 1999. [ bib ]
[17] Lilian Burdy, Yoonsik Cheon, David Cok, Michael Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An overview of JML tools and applications. Technical Report NIII-R0309, Dept. of Computer Science, University of Nijmegen, 2003. [ bib ]
[18] Lilian Burdy and Antoine Requet. Jack : Java Applet Correctness Kit. In Gemplus Developers Conference GDC'2002, 2002. [ bib ]
[19] Lilian Burdy, Antoine Requet, and Jean-Louis Lanet. Java applet correctness : a developer-oriented approach. In Keijiro Araki, Stefania Gnesi, and Dion Mandrioli, editors, FME 2003: International Symposium of Formal Methods Europe, volume 2805 of LNCS, pages 422-439, 2003. [ bib ]
[20] N. Cataño and M. Huisman. Formal specification and static checking of Gemplus's electronic purse using ESC/Java. In L.-H. Eriksson and P.A. Lindsay, editors, Proc. Formal Methods Europe FME'02, number 2391 in LNCS, pages 272-289. Springer-Verlag, 2002. [ bib ]
[21] N. Cataño and M. Huisman. Chase: a Static Checker for JML's Assignable Clause. In L.D. Zuck, P.C. Attie, A. Cortesi, and S. Mukhopadhyay, editors, Verification, Model Checking and Abstract Interpretation (VMCAI '03), number 2575 in LNCS, pages 26-40. Springer-Verlag, 2003. [ bib ]
[22] C. Darlot, J. Julliand, and O. Kouchnarenko. Refinement Preserves PLTL Properties. In 3nd International Conference of B and Z Users, ZB2003, à paraître. Springer-Verlag, 2003. [ bib ]
[23] David Déharbe and Sylvio Ranise. haRVey, 2002. http://www.loria.fr/equipes/cassis/softwares/haRVey. [ bib ]
[24] Jean-Christophe Filliâtre. The Why certification tool. http://why.lri.fr/. [ bib ]
[25] Mohamed Hibti, Henri Lombardi, and Bruno Legeard. Deciding in HFS-theory via linear integer programming. In Andrei Voronkov, editor, 4th International Conference, LPAR'93, volume 698 of LNCS, pages 170-181. Springer-Verlag, 1993. [ bib ]
[26] J. Julliand, P-A. Masson, and H. Mountassir. Vérification par model-checking modulaire des propriétés dynamiques introduites en B. Technique et Science Informatiques, 20(7), 2001. [ bib ]
[27] The Krakatoa team. The Krakatoa proof tool, 2002. http://www.lri.fr/~marche/krakatoa. [ bib ]
[28] J. Lebray. Modélisation de systèmes en B : Proposition de guides méthodologiques pour la décomposition d'événements. Rapport de DEA, Institut National Polytechnique de Grenoble, France, 2000. [ bib ]
[29] Claude Marché, Christine Paulin, and Xavier Urbain. The Krakatoa tool for JML/Java program certification. Available at http://krakatoa.lri.fr, 2003. [ bib | http ]
[30] J. Nahoum. Outils d'assistance à la construction de systèmes dans la méthode B. Rapport de DEA, Institut National Polytechnique de Grenoble, France, 2001. [ bib ]
[31] Marie-Laure Potet. Spécifications et développements formels: Etude des aspects compositionnels dans la méthode B. Habilitation à  diriger des  recherches, Institut National Polytechnique de Grenoble, 2002. [ bib ]
[32] Marie-Laure Potet. Spécifications et développements structurés dans la méthode B. In D. Bert, V. Donzeau-Gouge, and H. Habrias, editors, Développement rigoureux de logiciel avec la méthode B, volume 22. Technique et Science Informatiques, 2003. [ bib ]
[33] Marie-Laure Potet and Yves Rouzaud. Composition and Refinement in the B-Method. In D. Bert, editor, Proceedings of the Second International B Conference, volume 1393 of LNCS. Springer-Verlag, 1998. [ bib ]
[34] K. Trentelman and M. Huisman. Extending JML Specifications with Temporal Logic. In H. Kirchner and C. Ringeissen, editors, Proc. Int. Conf. on Algebraic Methodology And Software Technology AMAST'2002, number 2422 in LNCS, pages 334-348. Springer-Verlag, 2002. [ bib ]

This file has been generated by bibtex2html 1.85.