@INCOLLECTION{Wasserrab:08,
  author = {Daniel Wasserrab},
  title = {Towards Certified Slicing},
  booktitle = {Archive of Formal Proofs},
  publisher = {\url{http://isa-afp.org/entries/Slicing.shtml}},
  year = {2008},
  editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
  month = {September},
  ISSN = {2150-914x},
  note = {Formal proof development}
}

@INCOLLECTION{Wasserrab:09,
  author = {Daniel Wasserrab},
  title = {Backing up Slicing: Verifying the Interprocedural Two-Phase {H}orwitz-{R}eps-{B}inkley Slicer},
  booktitle = {Archive of Formal Proofs},
  publisher = {\url{http://isa-afp.org/entries/HRB-Slicing.shtml}},
  year = {2009},
  OPTeditor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
  month = {September},
  ISSN = {2150-914x},
  note = {Formal proof development}
}

@INPROCEEDINGS{WasserrabLS:09,
  author = {Daniel Wasserrab and Denis Lohner and Gregor Snelting},
  title = {On {PDG}-Based Noninterference and its Modular Proof},
  booktitle = {Proc. of PLAS '09},
  year = {2009},
  pages = {31--44},
  month = {June},
  OPTorganization = {PLAS 2009},
  publisher = {ACM},
  doi = {10.1145/1554339.1554345}
}

@InProceedings{BarthePR:07,
  author = 	 {Gilles Barthe and David Pichardie and Tamara Rezk},
  title = 	 {A Certified Lightweight Non-interference {Java} Bytecode Verifier},
  booktitle = 	 {ESOP 2007},
  year =         {2007},
  volume =       {4421},
  series =       {LNCS},
  pages =        {125-140},
  publisher =    {Springer},
  doi =          {10.1007/978-3-540-71316-6}
}

@ARTICLE{Kammueller:08,
  author = {Florian Kamm{\"u}ller},
  title = {Formalizing non-interference for a simple bytecode language in {Coq}},
  journal = {Formal Aspects of Computing},
  year = {2008},
  volume = {20},
  pages = {259--275},
  number = {3}
}

@ARTICLE{BartheN:04,
  author = {Gilles Barthe and Leonor Prensa Nieto},
  title = {Secure information flow for a concurrent language with scheduling},
  journal = {Journal of Computer Security},
  year = {2007},
  volume = {15},
  pages = {647--689},
  number = {6},
  publisher = {IOS Press}
}

@INCOLLECTION{BeringerH:08,
  author = {Lennart Beringer and Martin Hofmann},
  title = {Secure information flow and program logics},
  booktitle = {Archive of Formal Proofs},
  publisher = {\url{http://isa-afp.org/entries/SIFPL.shtml}},
  year = {2008},
  OPTeditor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
  month = {November},
  ISSN = {2150-914x},
  note = {Formal proof development}
}

@INCOLLECTION{SneltingW:08,
  author = {Gregor Snelting and Daniel Wasserrab},
  title = {A Correctness Proof for the {Volpano/Smith} Security Typing System},
  booktitle = {Archive of Formal Proofs},
  publisher = {\url{http://isa-afp.org/entries/VolpanoSmith.shtml}},
  year = {2008},
  editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
  month = {September},
  ISSN = {2150-914x},
  note = {Formal proof development}
}

@article{HammerS:09,
  author = {Christian Hammer and Gregor Snelting},
  title = {Flow-Sensitive, Context-Sensitive, and Object-sensitive Information	Flow Control Based on Program Dependence Graphs},
  year = {2009},
  publisher = {Springer},
  volume = {8},
  number = {6},
  pages = {399--422},
  journal = {International Journal of Information Security},
  doi = {10.1007/s10207-009-0086-1},
}

@ARTICLE{SabelfeldS:01,
  author = {Andrei Sabelfeld and David Sands},
  title = {A Per Model of Secure Information Flow in Sequential Programs},
  journal = {Higher Order Symbolic Computation},
  year = {2001},
  volume = {14},
  pages = {59--91},
  number = {1}
}