Context-Bounded Analysis of Concurrent Systems
- 14:00 7th June 2023 ( week 7, Trinity Term 2023 )Room 051
Context-bounded analysis of concurrent programs is a technique to compute a sequence of under-approximations of all behaviors of the program. For a fixed bound k, a context bounded analysis considers only those runs in which a single process is interrupted at most k times. As k grows, we capture more and more behaviors of the program. Practically, context-bounding has been very effective as a bug-finding tool: many bugs can be found even with small bounds. Theoretically, context-bounded analysis is decidable for a large number of programming models for which verification problems are undecidable.
I will survey some recent work in context-bounded analysis of multithreaded programs. I will show some general decidability results, and focus on some recent work on refinement verification with respect to non-regular properties.
Speaker bio
Rupak Majumdar is a Scientific Director at the Max Planck Institute for Software Systems. His research interests are in the verification and control of reactive, real-time, hybrid, and probabilistic systems, software verification and programming languages, logic, and automata theory. Dr. Majumdar received the President's Gold Medal from IIT Kanpur, the Leon O. Chua award from UC Berkeley, an NSF CAREER award, a Sloan Foundation Fellowship, an ERC Synergy award, a Distinguished Alumnus Award from IIT Kanpur, "Most Influential Paper" awards from PLDI and POPL, and several best paper awards. He received the B.Tech. degree in Computer Science from the Indian Institute of Technology at Kanpur and the Ph.D. degree in Computer Science from the University of California at Berkeley.Share this:
