Java Model Checking








The Java programming language is becoming 
increasingly popular for writing multi-threaded applications. In 
particular, many Internet servers are written in 
Java. Developing multi-threaded programs is notoriously difficult, 
however. Subtle program errors can result from 
unforeseen interactions among multiple threads. We describe 
a model checking tool for multi-threaded Java 
software that automatically detects deadlocks and assertion 
violations. The tool employs several techniques that 
we found effective in helping to deal 
with the typically huge number of reachable 
states. We give runtimes and memory requirements 
for several Java sample programs.