Modular verification of concurrent programs with heap

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

• Alexey Gotsman (ARG)
• Tuesday 03 March 2009, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Automated Reasoning Group Lunches
• Computer Laboratory, William Gates Building, Room SS03
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.