This paper presents a practical Java program analysis framework obtained by combining an extended verification toolbox with a Java virtual machine. In our methodology, rules are used to specify complex interprocedural program analyses involving dynamically created objects. After extracting an initial set of information about Java program semantics from the program Bytecode, our framework transforms the rules of a particular analysis into a Boolean Equation System (Bes), whose local resolution corresponds to the demand-driven computation of program analysis results.