Verification Challenges
Modern programming languages, such as Java, make extensive use of the heap to dynamically allocate and deallocate objects and threads. These languages also provide concurrency constructs to control thread scheduling and synchronization. The combination of concurrency with dynamic allocation of objects and threads on the heap creates an extremely challenging environment for verification.
All of the challenges listed here were solved using our verification techniques. When solving these problems, we made no additional assumptions on the number of allocated objects and/or threads. To the best of our knowledge, no other automatic verification techniques were able to successfully solve these challenges.