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.
Also read: The Suraksha of detecting gas leakages
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.
To read more about his work, click here