Date Added: Mar 2012
In this paper, the authors discuss and define an information flow property for sequential Java that takes into account information leakage through objects (as opposed to primitive values). They present proof rules for compositional reasoning over information-flow in Java programs. Their calculus rules apply at Java code-level (not at an abstraction), and they tie in with rules for functional verification. The new proof rules can be added to a Dynamic Logic calculus, as used in the KeY program verification system. The expressiveness of Dynamic Logic allows to specify and verify complex properties with high precision.