biblio-outils.bib

@BOOK{BBook,
  author = {Jean-Raymond Abrial},
  title = {The B-Book, assigning programs to meaning},
  publisher = {Cambridge University Press},
  year = 1996
}
@BOOK{Wordsworth,
  author = {J.B. Wordsworth},
  title = {Software Engineering with B},
  publisher = {Addison-Wesley},
  year = 1996
}
@MISC{AtelierB,
  key = {Atelier-B},
  title = {Site WEB de l'atelier {B}},
  note = {\url{http://www.atelierb.societe.com}}
}
@MISC{SiteB,
  key = {Site-B},
  title = {Site WEB sur {B}},
  note = {\url{http://www-lsr.imag.fr/B}}
}
@MISC{BTool,
  key = {B-Tool},
  title = {Site WEB de {B Tool}},
  note = {\url{http://www.b-core.com/btool.html}}
}
@MISC{JML,
  key = {JML},
  title = {Site WEB de {JML}},
  note = {\url{http://www.jmlspecs.org}}
}
@BOOK{Monin,
  author = {J.-F. Monin},
  title = {Comprendre les méthodes formelles},
  publisher = {Masson},
  year = 1996,
  series = {Collection technique et Scientifique des Télécommunications}
}
@BOOK{Spivey,
  author = {J. M. Spivey},
  title = {Understanding Z. A specification language and its formal seman
tics},
  publisher = {Cambridge University Press},
  year = 1988,
  volume = 3,
  series = {Cambridge Tracts in Theoretical Computer Science}
}
@INPROCEEDINGS{leavens00jml,
  author = {Gary T. Leavens and K. Rustan M. Leino and Erik Poll
                 and Clyde Ruby and Bart Jacobs},
  title = {{JML}: notations and tools supporting detailed design in {Java}},
  booktitle = {{OOPSLA} 2000 Companion, Minneapolis, Minnesota},
  pages = {105--106},
  year = 2000
}
@TECHREPORT{leavens00preliminary,
  author = {Gary T. Leavens and Albert L. Baker and Clyde Ruby},
  title = {Preliminary Design of {JML}: {A} Behavioral Interface 
           Specification Language for {Java}},
  institution = {Iowa State University},
  number = {98-06i},
  year = 2000
}
@TECHREPORT{raghavan00desugaring,
  author = {Arun D. Raghavan and Gary T. Leavens},
  title = {Desugaring {JML} Method Specifications},
  institution = {Iowa State University},
  number = {00-03a},
  year = 2000
}
@INPROCEEDINGS{vandenberg2001,
  author = {{Berg}, Joachim van den  and Bart Jacobs},
  title = {The {LOOP} compiler for {Java} and {JML}},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Software},
  pages = {299--312},
  year = 2001,
  editor = {T. Margaria and W. Yi},
  volume = 2031,
  series = {LNCS},
  publisher = {{Sprin\-ger-Verlag}}
}
@MISC{LoopProject,
  author = {{LOOP} Team, The},
  title = {Loop Project},
  note = {\url{http://www.cs.kun.nl/~bart/LOOP}},
  url = {http://www.cs.kun.nl/~bart/LOOP}
}
@TECHREPORT{labeth2000rr,
  author = {Labeth, M. and Meyer, J. and M{\"u}ller, P. and 
                 Poetzsch-Heffter, A. },
  title = {{Formal Verification of a Doubly Linked List Implementation: 
                 A Case Study Using the {\sc Jive} System} },
  institution = { Fernuniversit\"at Hagen },
  year = 2000,
  number = { 270 },
  url = {http://softech.informatik.uni-kl.de/en/publications/casestudy.ht
ml}
}
@UNPUBLISHED{meyer2000,
  author = {Meyer, J. and M{\"u}ller, P. and Poetzsch-Heffter, A. },
  title = {The {\sc Jive} System---Implementation Description },
  year = 2000,
  url = {http://www.informatik.fernuni-hagen.de/pi5/publications.html},
  note = {Available from \url{http://www.informatik.fernuni-hagen.de/pi5/public
ations.html}}
}
@MISC{ESC,
  title = {{ESC/Java} Home Page},
  key = {Esc/Java},
  year = 2002,
  note = {\url{http://research.compaq.com/SRC/esc}}
}
@MISC{SLAM,
  author = {Thomas Ball and Sriram K. Rajamani},
  title = {SLAM},
  year = 2002,
  note = {\url{http://research.microsoft.com/slam}}
}
@TECHREPORT{LeinoNS00,
  author = {K.R.M. Leino and G. Nelson and J.B. Saxe},
  title = {{ESC/Java} User's Manual},
  institution = {Compaq System Research Center},
  number = {SRC 2000-002},
  year = 2000
}
@INPROCEEDINGS{bartetzko01assertions,
  author = {D. Bartetzko and C. Fischer and M. M{\"o}ller and 
              H. Wehrheim},
  title = {{Jass~{--}~Java with Assertions}},
  booktitle = {Electronic Notes in Computer Science},
  volume = {55(2)},
  publisher = {Elsevier Science BV},
  editor = {K. Havelund and G. Ro\c su},
  year = {2001}
}
@INPROCEEDINGS{BreunesseJB02,
  title = {{Specifying and Verifying a Decimal Representation in Java 
for Smart Cards}},
  author = {C. Breunesse and B. Jacobs and Berg, J. van den},
  year = 2002,
  booktitle = {Proc. Int. Conf. on Algebraic Methodology And Software Technology AMAST'2002},
  publisher = {Springer-Verlag},
  pages = {304--318},
  series = {LNCS},
  number = 2422,
  editor = {H. Kirchner and C. Ringeissen}
}
@ARTICLE{poll01cn,
  author = {Erik Poll and Berg, Joachim van den  and Bart Jacobs},
  title = {Formal Specification of the {JavaCard API in JML}: the {APDU class}},
  journal = {Computer Networks},
  year = 2001,
  volume = 36,
  number = 4,
  pages = {407-421}
}
@BOOK{Gamma1995,
  author = {Erich Gamma and Richard Helm and Ralph Johnson and John
Vlissides},
  title = {Design Patterns: Elements of Reusable Object-Oriented
Software},
  year = 1995,
  publisher = {{ Addison-Wesley} Publishing Company},
  series = {{ Addison-Wesley} Professional Computing Series},
  address = {New York, NY}
}
@TECHREPORT{BuechiWeck99,
  author = {Martin B{\"u}chi and Wolfgang Weck},
  title = {The Greybox Approach: When Blackbox Specifications
Hide Too Much},
  institution = {Turku Center for Computer Science},
  number = {297},
  url = {\verb!http://www.tucs.fi/Publications/techreports/TR297.php!},
  month = {August},
  year = 1999
}
@TECHREPORT{back00class,
  author = {Ralph-Johan Back and Anna Mikhajlova and Joakim von Wright},
  title = {Class Refinement as Semantics of Correct Object Substitutability},
  institution = {Turku Center for Computer Science},
  number = {333},
  url = {\verb!http://www.tucs.fi/Publications/techreports/TR333.php!},
  year = {2000}
}
@PHDTHESIS{utting92objectoriented,
  author = {Mark Utting},
  title = {An Object-Oriented Refinement Calculus with Modular
Reasoning},
  school = {University of New South Wales},
  address = {Kensington, Australia},
  year = {1992}
}
@TECHREPORT{MikhajlovReentrance,
  author = {Leonid Mikhajlov},
  title = {Developing Components in the Presence of Re-entrance},
  institution = {Turku Center for Computer Science},
  number = {239},
  url = {\verb!http://www.tucs.fi/Publications/techreports/TR239.php!},
  month = {February},
  year = 1999
}
@INPROCEEDINGS{Bornat00,
  author = {Richard Bornat},
  title = {Proving pointer programs in {Hoare} Logic},
  booktitle = { Mathematics of Program Construction, 5th International Conference, MPC'2000},
  year = 2000,
  editor = {R. Backhouse and J. N. Oliveira},
  volume = {1837},
  series = {LNCS},
  publisher = {{Sprin\-ger-Verlag}}
}
@INPROCEEDINGS{Nipkow03,
  author = {Farhad Mehta and Tobias Nipkow},
  title = {Proving Pointer Programs in Higher-Order Logic},
  booktitle = {Automated Deduction - CADE-19},
  year = 2003,
  series = {LNCS},
  publisher = {{Sprin\-ger-Verlag}}
}
@ARTICLE{JacobsPoll02,
  author = {Bart {Jacobs} and Erik {Poll}},
  title = {Coalgebras and monads in the semantics of {Java}},
  journal = {Theoretical Computer Science},
  volume = 291,
  pages = {329--349},
  year = 2002
}
@BOOK{REFINEMENT,
  author = {Ralph-Johan {Back} and Joakim von {Wright}},
  title = {Refinement Calculus: A Systematic Introduction},
  publisher = {Springer-Verlag},
  year = {1998}
}

This file has been generated by bibtex2html 1.85.