Modular verification of concurrent programs with heap

Reasoning about concurrent programs is made difficult by the number of possible interactions between threads. This is especially true for heap-manipulating programs, in which threads can interact in subtle ways via dynamically-allocated data structures. I will present novel thread-modular logics and analyses for concurrent heap-manipulating programs that address this challenge. The logics and the analyses can be used to reason about or automatically verify a number of safety properties (memory safety, data race freedom, absence of memory leaks) and have been successfully used as a key ingredient in methods for verifying liveness properties. I will also discuss my approach to their design in which program logics and program analyses share the underlying reasoning principles.