Research
I am working on the formal verification of
concurrent reactive systems - hardware, protocols and distributed algorithms.
I worked on the symbolic model checker
VIS.
Since 1997, I have been working on a new model checker
MOCHA
that leverages off the symbolic state exploration engine of VIS and provides additional support for
compositional reasoning under the assume-guarantee paradigm and model checking the temporal logic
ATL (Alternating-time temporal logic). You can get more information about Mocha in the following paper.
- R. Alur, T. A. Henzinger, F. Y. C. Mang, S. Qadeer, S. K. Rajamani, S. Tasiran.
MOCHA: Modularity in Model Checking.
Proceedings of the 10th International Conference on Computer-Aided Verification, 1998.
Postscript.
I have been working in the following areas.