Author =   {L. Burdy and A. Requet and J.-L. Lanet},
   Title =    {Java Applet Correctness: A Developer-Oriented Approach},
   Booktitle = {FME 2003: Formal Methods: International Symposium of Formal Methods Europe},
   Editor =   {K. Araki and S. Gnesi and D. Mandrioli},
   Volume =   {2805},
   Series =   {Lecture Notes in Computer Science},
   Pages =    {422--439},
   Publisher = {Springer-Verlag},
   Year =     {2003},
   PSurl =    {ftp://ftp-sop.inria.fr/everest/publis/2003/BRL03fme.ps.gz}

  AUTHOR =   {G. Barthe and P. D'Argenio and T. Rezk},
  TITLE =    {{Secure Information Flow by Self-Composition}},
  CROSSREF = {csfw04},
  PAGES =    {100-114},
  TOPICS =   {team}

  AUTHOR =   {M. Pavlova and G. Barthe and L. Burdy and M. Huisman and J.-L. Lanet},
  TITLE =    {Enforcing High-Level Security Properties For Applets},
  CROSSREF = {cardis04},
  PAGES =    {},
  TOPICS =   {team}

  author =   {G. Barthe and M. Pavlova and G. Schneider},
  title =    {{Precise analysis of memory consumption using program logics}},
  year =     {2005},
  note=      {Manuscript}

  title=     {Java Bytecode Specification and Verification},
  author=    {L. Burdy and M. Pavlova},
  note=      {Manuscript},
  year=      {2005}

  author =    {Julien Charles},
  title =     {Adding Native Specifications to {JML}},
  booktitle = {ECOOP workshop on Formal Techniques for Java-like Programs (FTfJP2006)},
  year =     2006, 

  author = {G. Barthe and L. Burdy and J. Charles and B. Gr{\'e}goire and M. Huisman and J.-L. Lanet and M. Pavlova and A. Requet},
  title = {{JACK}:  a tool for validation of security and behaviour of {Java} applications},
  booktitle = {FMCO: Proceedings of 5th International Symposium on Formal Methods for Components and Objects},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  year = {2007},
  note = {To appear},
  pdfurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/fmco06.pdf},
  topics = {team}