Formal Verification of Components in Java

The full text of the thesis can be downloaded here. It is a collection of papers with unifying text.
All techniques proposed in the thesis are implemented in the COMBAT toolset.