@InProceedings{fred04:rv,
  author =       {L.-A. Fredlund},
  title =        {Guaranteeing Correctness Properties of a Java Card Applet},
  booktitle =    {Proceedings of {RV}'04},
  pages =     {217-233},
  year =         {2004},
  editor =    {K.~Havelund and G.~Rosu},
  volume =    {113},
  series =       entcs,
  publisher = elsevier,
}

@inproceedings{WCN05:bytecode,
  author =  {M. Wildmoser and A. Chaieb and T. Nipkow},
  title =   {Bytecode Analysis for Proof Carrying Code},
  booktitle = {Proceedings of BYTECODE'05},
  year =    2005,
  editor={F.~Spoto},
series=entcs,
publisher=elsevier}
}


@inproceedings{CL05:jot,
title="Inferring object invariants",
author="B.-Y.E. Chang and K.R.M. Leino",
booktitle={Proceedings of {AIOOL}'05},
year={2005},
editor={A.~Cortesi and F.~Logozzo},
publisher=elsevier,
series=entcs,
note={To appear}}


@inproceedings{igor05:qapl,
  author = {I. Siveroni},  
  title = {{Filling out the Gaps: A Padding Algorithm for Transforming Out Timing Leaks}},
  year = 	 {2005},
booktitle={Proceedings of {QAPL}'05},
editor={A. Cerone and H. Wiklicky},
publisher=elsevier,
series=entcs,
note={To appear}}


@inproceedings{BM05:bytecode,
author={F. Bannwart and P. M\"uller},
title={A Program Logic for Bytecode},
booktitle={Proceedings of {B}ytecode'05},
editor={F. Spoto},
 series=entcs,
    publisher = elsevier,
year={2005}}

@inproceedings{jass01:rv,
    author = {D. Bartetzko and C. Fischer and M. M{\"o}ller and 
              H. Wehrheim},
    title = {{Jass~{--}~Java with Assertions}},
    booktitle = "Proceedings of RV'01",
    volume = {55},
    issue=2,
    series=entcs,
    publisher = elsevier,
    editor = {K. Havelund and G. Ro\c su},
    year = {2001}
}


@INPROCEEDINGS{lilian+03:fmics,
   Author = {L. Burdy and Y. Cheon and D. Cok and M. Ernst and J. Kiniry and G. T. Leavens and K. R. M. Leino and E. Poll},
   Title = "An overview of JML tools and applications",
   Booktitle = "Proceedings of {FMICS'03}",
   Editor = {T. Arts and W. Fokkink},
   Volume = {80},
   Series = entcs,
   Publisher = {Elsevier Publishing},
   Year = {2003}}


@InProceedings{HR01:rv,
  author =       "K. Havelund and G. Rosu",
  title =        "Monitoring {Java} Programs with {Java PathExplorer}",
  booktitle =    "Proceedings of RV'01",
  year =         "2001",
  editor =       "K. Havelund and G. Ro{\c{s}}u",
  volume =       "55",
  issue =        "2",
  series =       entcs,
  publisher =    "Elsevier Publishing"
}


@inproceedings{zwa03:mfps,
author={S. Zwandewic},
title={A Type System for Robust Declassification},
booktitle={Proceedings of {MFPS}'03},
editor={S. Brookes and P. Panangaden},
series=entcs,
volume={83},
publisher=elsevier,
year={2003}}


@inproceedings{CBC02:fwan,
title={Information Flow Security for Boxed Ambients},
author={S. Crafa and M. Bugliesi and G. Castagna},
booktitle={Proceedings of {F-WAN}},
editor={V. Sassone},
series=entcs,
volume={66(3)},
publisher=elsevier,
year={2002}}