|
Alexey Gotsman University of Cambridge |
|
Modular verification of concurrent programs with heap The trend in software design is towards additional concurrency. A problem with this trend is that programmers find it difficult to write correct concurrent programs, especially when the programs are manipulating shared data structures. Automatic verification methods could ameliorate this problem. However, verifying concurrent programs is difficult because of the need to consider all possible interactions among concurrently executing threads. Their tractable verification is possible with modular reasoning techniques, which sidestep this difficulty by considering every thread in isolation under some assumptions on its environment. The difficulty with this approach is the current lack of practical techniques that can verify a wide spectrum of properties and handle modern programming language features. I will present novel 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. ********** Alexey Gotsman is a PhD candidate at the University of Cambridge (UK) supervised by Byron Cook and Mike Gordon. His research interests are in the area of formal verification, particularly, in logical foundations and practical tools for verifying concurrent software. During his PhD he has interned at Microsoft Research Cambridge and Cadence Berkeley Labs. . |
|
4:15pm 5130 Upson Hall Tuesday, April 21, 2009 Refreshments at 3:45pm in the Upson 4th Floor Atrium |
|
Computer Science Colloquium Spring 2009 |
|
www.cs.cornell.edu/events/colloquium |