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.

For one thing, it is not even clear how to specify the behavior of such programs in a way that allows addressing both the temporal and spatial aspects of their behavior. But even when these properties are eventually specified, actually verifying them requires new and sophisticated verification algorithms.

In our research, we have established a specification languge named Evolution Temporal Logic (ETL), which is a first-order temporal logic, for specifying properties of heap-manipulating programs.

We have also presented several techniques for verifying such specifications.

Finally, we have applied our techniques to verify properties of interesting Java programs,  such as the correctness of concurrent queue algorithms, properties of web-server prototypes, and even properties for compile-time memory management.

[See verification challenges page for related interesting verification problems]

[See publications page for more details]