This is an unofficial reimagining of the Archive of Formal Proofs
A Bytecode Logic for JML and Typesby Lennart Beringer and Martin Hofmann
Secure information flow and program logicsby Lennart Beringer and Martin Hofmann