IMDEA Software

IMDEA initiative

Home > Events > Invited Talks > 2009 > Modular verification of concurrent programs with heap

Alexey Gotsman

Thursday, March 5, 2009

11:00am Amphitheatre H-1001

Alexey Gotsman, PhD candidate, University of Cambridge, United Kingdom

Modular verification of concurrent programs with heap

Abstract:

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.