A Java-like formalism for control flow analysis.

I'm looking into defining a flow-sensitive effects system for Java (to check things like the definite assignment of local variables). Does anybody know of a good existing Java-like formalism I could use?

I don't think Featherweight Java is appropriate here because it mostly ignores Java's control-flow mechanisms. Much of what's interesting about a flow-sensitive effects system has to do with loops, conditionals, exceptions. On the other hand, I care less about things like classes and inheritance.

Maybe the simply typed lambda calculus (plus some Java-like exception mechanism) would work better?