http://www.tcs.informatik.uni-muenchen.de/~mhofmann
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