If you would like to automatically verify properties of Java source code, you should consider using Bandera to model-check these properties. The strength of model-checking is its ability to aid in detection of subtle software defects due to unanticipated interleaving of concurrently executing threads. One can also use model-checking to check assertions, pre/post-conditions, and simple data invariants. However, it must be remembered that model-checking will always work better for verifying control-related properties rather than data-related properties. The more data-related a property is, the larger the state-space becomes, and thus resources required for model-checking. Model-checking has been used to verify data properties related to ``container'' objects like stacks and queues. For example, it can be used to show that the code for a stack does indeed maintain a LIFO ordering [4]. However, it seems impossible to use model-checking to verify that a sorting algorithm is correct since sorting correctness is a data-oriented property involving several quantifications and data structures. For verifying this type of property, other formal methods such as theorem proving would need to be used. Similarly, other verification problems such as checking for array-bounds errors, buffer overruns, and null-pointer dereference probably are best done using other forms of static dataflow analysis.
If you would like to slice and perform data abstraction on Java programs, you should consider using Bandera. Slicing and data abstraction are also useful techniques for analysis and testing. Since Bandera can carry out both slicing and abstraction as source-to-source transformations, you can bypass Bandera's back-end for model-checking and instead use transformed Java files as the input to, e.g., a testing tool.
If you have a model-checker that you would like to use to check Java source code, you should consider incorporating it into Bandera by writing a translation from BIR to the input language of the model-checker.