Verifying LTL Properties Using 3-Valued Logic

Eran Yahav, Thomas Reps, and Mooly Sagiv

The stumbling block 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 in size unboundedly. This paper presents a method for verifying LTL properties of concurrent Java programs. 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 programs that dynamically allocate thread objects, and even programs that create an unbounded number of threads.