University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > Modular verification of concurrent programs with heap

Modular verification of concurrent programs with heap

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Thomas Tuerk.

Mike Hick's talk moved to the 17th of March

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.

This is a rehearsal of my job talk. The talk does not contain any new results: all the results have already been presented at previous ARG Lunches.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity