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.