I am a graduate student in the EECS department at UC, Berkeley (2013 - present).
I am extremely fortunate to be co-advised by Sanjit Seshia and Shaz Qadeer.
Before joining the graduate school, I had the privilege of spending 2+ years at Microsoft Research (India) working with Sriram Rajamani and Shaz Qadeer, and getting trained for the graduate school ☺.
During my time at IIT, Kanpur, I was part of the team that built the first Indian Nano-Satellite JUGNU, and we had lots of (fun -- Pictures). The satellite was successfully launched on 12 October 2011 . I lead the On-Board Computers team designing and implementing the software stack for the satellite (please check out my master's thesis).
My research focuses on combining techniques from programming languages, formal methods, and software engineering for building reliable systems. I have designed tools and methodologies for building reliable systems across domains like device drivers, fault-tolerant distributed systems, robotics and cyber-physical systems.
Programming Languages and Frameworks
I have designed and implemented the following tools and frameworks:
P Programming Language [P on GitHub]P is a language for asynchronous event-driven programming. P allows the programmer to specify the system as a collection of interacting state machines, which communicate with each other using events. P unifies modeling and programming into one activity for the programmer. We have made P modular by implementing a module system that allows compositional programming and assume-guarantee syle reasoning of P programs. Not only can a P program be compiled into executable code, but it can also be validated using systematic testing. P has been used to implement and validate the USB device driver stack that ships with Microsoft Windows 8 and Windows Phone. P is also used for the design and implementation of networked, embedded, and distributed systems.
DRONA: Programming Safe Robotics Systems [Drona-Webpage]We built DRONA, a software framework for safe distributed mobile robotics systems. DRONA uses P language for implementing and model-checking the distributed robotics software stack. We extended P with Runtime Assurance capabilities to guarantee safe operation of the autonomous robot, especially when the assumptions made during design-time verification are violated. The C code generated from compiler can be easily deployed on Robot Operating System (ROS). More details about the DRONA framework and simulation videos are available at the website
Zing : An explicit state model checker for concurrent and message passing programs.[Zing on GitHub]The goal of the Zing project is to build a flexible and scalable systematic state space exploration infrastructure for software. Zing is a flexible and scalable (parallel exploration)infrastructure for exploring states of concurrent software systems. Zing was used for model-checking drivers for Windows and Windows Phone. It supports state-of-the-art delay bounding based search prioritization and MaceMC like liveness checking