I am Aws Albarghouthi, a graduate student at the University of Toronto. Last summer, I interned at Microsoft Research in Bangalore, India with Aditya Nori and Sriram Rajamani. In a few weeks, I will be at PLDI presenting our work on parallelizing a large class of top-down interprocedural analyses.
Top-down analyses typically compute summaries for procedures according to a given calling context. They start with the main function, working their way down and analyzing functions according to the calling context in which they are called by their callees. Our key insight is a MapReduce-like technique for distributing analyzing different calling contexts of different procedures to different processor cores. Come to the talk and hear about the exciting experiments and speedups we achieved in verifying Windows device drivers.
This work is part of a bigger verification project, called Yogi, where testing and static analysis are combined to produce efficient verification techniques. Aditya and Sriram will be giving a tutorial on it on June 16th. Be there!