Ankush Desai

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