publis.bib

@MISC{krakatoa02,
  author = {{Krakatoa team}, The},
  title = {The \textsf{Krakatoa} proof tool},
  year = 2002,
  note = {\url{http://www.lri.fr/~marche/krakatoa}}
}
@MISC{HARVEY,
  author = {David D\'eharbe and Sylvio Ranise},
  title = {{haRVey}},
  year = 2002,
  note = {\url{http://www.loria.fr/equipes/cassis/softwares/haRVey}}
}
@UNPUBLISHED{krakatoa03a,
  author = {Claude March\'e and Christine Paulin and Xavier Urbain},
  title = {The {Krakatoa} Tool for {JML/Java} Program Certification},
  year = 2003,
  note = {Available at \url{http://krakatoa.lri.fr}},
  url = {http://krakatoa.lri.fr}
}
@INPROCEEDINGS{CatanoH03,
  title = {{Chase: a Static Checker for JML's Assignable Clause}},
  author = {N. Cata{\~n}o and M. Huisman},
  year = 2003,
  booktitle = {Verification, Model Checking and Abstract Interpretation 
(VMCAI '03)},
  editor = {L.D. Zuck and P.C. Attie and A. Cortesi and S. 
Mukhopadhyay},
  series = {LNCS},
  number = 2575,
  pages = {26--40},
  publisher = {Springer-Verlag}
}
@INPROCEEDINGS{CatanoH02a,
  title = {Formal Specification and Static Checking of {Gemplus's} 
Electronic Purse Using {ESC/Java}},
  author = {N. Cata{\~n}o and M. Huisman},
  year = 2002,
  booktitle = {Proc. Formal Methods Europe FME'02},
  editor = {L.-H. Eriksson and P.A. Lindsay},
  series = {LNCS},
  publisher = {Springer-Verlag},
  number = {2391},
  pages = {272--289}
}
@INPROCEEDINGS{Jack02,
  author = {Lilian Burdy and Antoine Requet},
  title = {Jack : {Java Applet Correctness Kit}},
  booktitle = {Gemplus Developers Conference GDC'2002},
  year = 2002
}
@INPROCEEDINGS{burdy03fme,
  author = {Lilian Burdy and Antoine Requet and Jean-Louis Lanet},
  title = {Java Applet Correctness : a Developer-Oriented Approach},
  booktitle = {FME 2003:  International Symposium of Formal Methods Europe},
  pages = {422--439},
  year = 2003,
  editor = {Keijiro Araki and Stefania Gnesi and Dion Mandrioli},
  volume = 2805,
  series = {LNCS}
}
@ARTICLE{ARR03,
  author = {Alessandro Armando and Sylvio Ranise and Micha\"el Rusinowitch},
  title = {A Rewriting Approach to Satisfiability Procedures},
  journal = {Information and Computation},
  year = 2002,
  note = {\`A para\^{\i}tre}
}
@INPROCEEDINGS{BPR96,
  author = {Didier Bert  and Marie-Laure Potet and Yann Rouzaud},
  title = {{A study on components and assembly primitives in B}},
  booktitle = {Proc. of First B Conference},
  iplace = {IRIN, Nantes},
  editor = {H. Habrias},
  page = {47-62},
  month = {Novembre},
  year = {1996}
}
@INPROCEEDINGS{PR98,
  author = {Marie-Laure~Potet  and Yves~Rouzaud},
  title = {{Composition and Refinement in the {B}-Method}},
  publisher = {Springer-Verlag},
  series = {LNCS},
  volume = {1393},
  booktitle = {Proceedings of the Second International B Conference},
  editor = {D. Bert},
  year = {1998}
}
@PHDTHESIS{potet02a,
  author = {Marie-Laure Potet},
  title = {Sp\'ecifications et d\'eveloppements formels: Etude des aspects
compositionnels dans la m\'ethode B},
  type = {Habilitation \`a ~Diriger des ~Recherches},
  school = {Institut National Polytechnique de Grenoble},
  year = {2002}
}
@INPROCEEDINGS{potet02b,
  author = {Marie-Laure Potet},
  title = {{Sp\'ecifications et d\'eveloppements structur\'es dans la
m\'ethode
B}},
  publisher = {Technique et Science Informatiques},
  volume = {22},
  booktitle = {D\'eveloppement rigoureux de logiciel avec la m\'ethode B},
  editor = {D. Bert and V. Donzeau-Gouge and H. Habrias},
  year = {2003}
}
@INPROCEEDINGS{Ba03,
  author = {F. Badeau and D. Bert and S. Boulm\'e and M-L. Potet and N.
Stouls and L. Voisin},
  title = {{ Traduction de B vers des langages de programmation : points de
vue
du projet BOM}},
  booktitle = {Actes des Journ\'ees AFADL, IRISA, RENNES},
  month = {Janvier},
  year = {2003}
}
@MISC{Fisl03,
  author = {Sylvain {Boulm\'e}},
  title = {{\em Toward a High Order Functional and Imperative Specification
   Language}},
  howpublished = {Unpublished},
  month = FEB,
  year = 2003
}
@MISC{Smol02,
  author = {Sylvain {Boulm\'e}},
  title = {{\em Interpr\'etation de programmes orient\'es objet annot\'es
 en th\'eorie des types}},
  howpublished = {Etude pr\'eliminaire, non publi\'ee},
  month = DEC,
  year = 2002
}
@INPROCEEDINGS{Boulme00a,
  author = {Sylvain {Boulm\'e}},
  title = {Op\'erateurs de raffinement sur les structures alg\'ebriques},
  booktitle = {Journ\'ees Francophones des Langages Applicatifs},
  publisher = {INRIA},
  year = {2000},
  month = FEB
}
@INPROCEEDINGS{Boulme99,
  author = {Sylvain {Boulm\'e} and Th\'er\`ese {Hardin} and Renaud
{Rioboo}},
  title = {Modules, objets et calcul formel},
  booktitle = {Journ\'ees Francophones des Langages Applicatifs},
  publisher = {INRIA},
  year = {1999},
  month = FEB
}
@PHDTHESIS{Boulme-thesis,
  author = {Sylvain Boulm\'e},
  title = {{Sp\'ecification d'un environnement d\'edi\'e \`a la programmation
certifi\'ee
de biblioth\`eques de calcul formel}},
  school = {Universit\'e Paris~6},
  year = 2000,
  month = DEC
}
@ARTICLE{Boulme01,
  author = {Sylvain Boulm{\'e} and Gr{\'e}goire Hamon},
  title = {Certifying Synchrony for Free},
  journal = {LNCS},
  volume = {2250},
  year = {2001}
}
@INPROCEEDINGS{BC00,
  author = {Didier Bert and Francis Cave},
  title = {{Construction of Finite Labelled Transition Systems from B Abstract
Systems}},
  booktitle = {Integrated Formal Methods, IFM2000},
  pages = {235--254},
  year = {2000},
  series = {LNCS},
  volume = 1945,
  month = NOV,
  publisher = {Springer-Verlag}
}
@ARTICLE{JC:Bert01,
  author = {Didier Bert},
  title = {{Sp\'ecification alg\'ebrique et prototypage du << contr\^ole d'acc\`es >>
en LPG}},
  journal = {Technique et Science Informatiques},
  year = {2001},
  pages = {849-873},
  publisher = {Herm\`es},
  volume = {20},
  number = {7}
}
@INPROCEEDINGS{CNC:Bert01,
  author = {Didier Bert},
  title = {{Preuve de propri\'et\'es d'\'equit\'e en B : \'etude du protocole
du bus SCSI-3}},
  booktitle = {Actes de l'Atelier AFADL'2001},
  address = {LORIA, Nancy, France},
  pages = {221-241},
  year = {2001},
  month = JUN,
  editor = {J. Souqui\`eres}
}
@INPROCEEDINGS{RBB02,
  author = {Hector Ruiz Barradas and Didier Bert},
  title = {{Specification and Proof of Liveness Properties under Fairness
Assumptions in B Event Systems}},
  booktitle = {Integrated Formal Methods, IFM2002},
  pages = {360--379},
  series = {LNCS},
  volume = 2335,
  year = {2002},
  month = MAY,
  publisher = {Springer-Verlag}
}
@TECHREPORT{Nahoum01,
  title = {Outils d'assistance \`a la construction de syst\`emes dans la
m\'ethode {B}},
  author = {J. Nahoum},
  type = {Rapport de {DEA}},
  institution = {Institut National Polytechnique de Grenoble, France},
  year = {2001}
}
@TECHREPORT{Lebray00,
  title = {Mod\'elisation de Syst\`emes en {B} : Proposition de guides
m\'ethodologiques pour la d\'ecomposition d'\'ev\'enements.},
  author = {J. Lebray},
  type = {Rapport de {DEA}},
  institution = {Institut National Polytechnique de Grenoble, France},
  year = {2000}
}
@INPROCEEDINGS{Besancon-FASE2000,
  author = {F. Bellegarde and J. Julliand and O. Kouchnarenko},
  title = {{Ready-simulation is not Ready to Express a Modular Refinement
Relation}},
  booktitle = {Fundamental Aspects of Software Engineering 2000, FASE'2000},
  year = {2000},
  series = {LNCS},
  volume = 1783,
  publisher = {Springer-Verlag}
}
@INPROCEEDINGS{Besancon-FME2001,
  author = {F. Bellegarde and C. Darlotand  J. Julliand and O. Kouchnarenko},
  title = {{Reformulation : a Way to Combine Dynamic Properties and B
Refinement}},
  booktitle = {FME 2001 ("Formal Methods Europe")},
  year = {2001},
  series = {LNCS},
  volume = 2021,
  publisher = {Springer-Verlag}
}
@INPROCEEDINGS{Besancon-ZB2002,
  author = {F. Bellegarde and J. Julliand and O. Kouchnarenko},
  title = {{Synchronized Parallel Composition of Event Systems in B}},
  booktitle = { 2nd International Conference of B and Z Users, ZB2002},
  series = {LNCS},
  volume = 2272,
  year = {2002},
  publisher = {Springer-Verlag}
}
@INPROCEEDINGS{Besancon-ZB2003,
  author = {C. Darlot and J. Julliand and O. Kouchnarenko},
  title = {{Refinement Preserves PLTL Properties}},
  booktitle = { 3nd International Conference of B and Z Users, ZB2003, \`a
para\^{\i}tre},
  year = {2003},
  publisher = {Springer-Verlag}
}
@ARTICLE{Besancon-TSI2001,
  author = {J. Julliand and  P-A. Masson and H. Mountassir},
  title = {{V\'erification par model-checking modulaire des propri\'et\'es dynamiques introduites en B}},
  journal = {Technique et Science Informatiques},
  year = 2001,
  volume = 20,
  number = 7,
  editor = {D. Bert and V. Donzeau-Gouge and H. Habrias}
}
@TECHREPORT{BurdyEtAl03,
  author = {Lilian Burdy and Yoonsik Cheon and David Cok and 
                   Michael Ernst and Joe Kiniry and Gary T. Leavens and 
                   K. Rustan M. Leino and Erik Poll},
  title = {An overview of {JML} tools and applications},
  institution = {Dept. of Computer Science, University of Nijmegen},
  year = {2003},
  number = {NIII-R0309}
}
@MISC{why,
  author = {Jean-Christophe Filli{\^a}tre},
  title = {The {Why} certification tool},
  note = {\url{http://why.lri.fr/}}
}
@INPROCEEDINGS{Huis02,
  title = {{Extending JML Specifications with Temporal Logic}},
  author = {K. Trentelman and M. Huisman},
  year = 2002,
  booktitle = {Proc. Int. Conf. on Algebraic Methodology And Software Technology AMAST'2002},
  publisher = {Springer-Verlag},
  series = {LNCS},
  pages = {334-348},
  number = 2422,
  editor = {H. Kirchner and C. Ringeissen}
}
@INPROCEEDINGS{HLL93,
  author = {Hibti, Mohamed and Lombardi, Henri and Legeard,
                  Bruno},
  title = {Deciding in {HFS}-theory via linear integer
                  programming},
  editor = {Voronkov, Andrei},
  booktitle = {4th International Conference, LPAR'93},
  volume = {698},
  series = {LNCS},
  pages = {170--181},
  publisher = {{Sprin\-ger-Verlag}},
  year = {1993}
}

This file has been generated by bibtex2html 1.85.