Akash Lal, 29
Improving software quality using automated verification
With software becoming all pervasive in our daily lives, it must become all the more reliable and shouldn't crash or behave unexpectedly. And the way to address this is through automated verification of programs. Though automated verification can significantly improve the quality of software with little manual effort, the available verification tools have been used to test sequential programs. This is a concern as modern software is invariably concurrent.
The problem of automatically verifying concurrent programs is two-fold: one has to explore different inputs to the program, and also explore different interleavings that happen between threads in the program for each input. Akash Lal's work shows that verification of real-world concurrent programs is possible. His innovation bridges the worlds of sequential and concurrent programs. He has shown how a concurrent program can be efficiently transformed to a sequential one under certain conditions. Lal, along with his colleagues at Microsoft Research Lab in Bangalore, has built a tool called Poirot that is capable of finding bugs in real-world concurrent programs that are missed by conventional testing.
"Akash's research has created an opportunity for developing precise and scalable tools for analyzing concurrent software, and many researchers including me are building on top of his work," says Shaz Qadeer, Lal's colleague at Microsoft, Redmond. Using a collection of models of concurrent programs, Lal's approach is 30 times faster than any existing tool for verifying concurrent programs.