Talks & Seminars
Title: Verification of Concurrent Programs
Dr. Ashutosh Gupta,
Date & Time: October 10, 2013 16:00
Venue: Lecture Hall, B Block, 03rd Floor, Department of Computer Science and Engineering, Kanwal Rekhi Building
Concurrent programs are notoriously difficult to get right. In this talk I will present two pieces of work for verification of concurrent program. In first work, we presented a novel algorithm for verification of concurrent programs using compositional reasoning. To enable scalable compositional reasoning, our algorithm requires explicit identification of the interplay between processes, so-called environment transitions. Once the environment transitions are identified, we verify each process in isolation, as the environment transitions keep track of the interleavings with other processes. Our algorithm is designed to find adequate environment transitions that are sufficiently precise to yield results and yet do not overwhelm the verifier with unnecessary details. We built a tool called THREADER based on our algorithm. THREADER has participated in the concurrency track of the competition on software verification in 2012 and 2013 and has won *Bronze and Gold medals* respectively. In another work, we focused on verification of the data structures in concurrent programs that allow concurrent operations with certain correctness guarantees. The search for new concurrent data structures that maximize the degree of concurrency among the operations is an active research area. Due to the innovative optimizations in the latest data structures, there has been limited success in their automatic verification. We have developed a novel algorithm to automatically verify some of the latest data structures that increase concurrency by allowing concurrent operations to coordinate and compute their combined effect, and then apply the combined effect on the shared data as a single operation.
Speaker Profile:
List of Talks


Faculty CSE IT
Forgot Password
    [+] Sitemap     Feedback