Treffer: Finite Model Generation for Distributed Java Programs

— We present techniques for analyzing the source code of distributed Java applications, and building finite models of their behaviour. The models are labelled transition systems, representing the communication events between the distributed objects. When combined with techniques for abstracting the data values used by the programs, and especially values used in the creation of distributed objects, to bounded domains, our construction terminates. We provide models suitable for automatic verification, and typically for model checking. Moreover our models are structured in a compositionnal way, so that we can use verification techniques that scale up to applications of realistic size. I.