Ankush Desai
About Me
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).
More details in my [CV]
Research Summary
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