One of the stumbling blocks to applying model checking to a concurrent language such as Java is that a program's data structures (as well as the number of threads) can grow and shrink dynamically, with no fixed upper bound on their size or number. This paper presents a method for verifying LTL properties of programs written in such a language. It uses a powerful abstraction mechanism based on 3-valued logic, and handles dynamic allocation of objects (including thread objects) and references to objects. This allows us to verify many programs that dynamically allocate thread objects, and even programs that create an unbounded number of threads.

(Click here to access the paper: PostScript, PDF.)