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).

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

Publications (Google Scholar)

SOTER: Programming Safe Robotics System using Runtime Assurance

Ankush Desai, Shromona Ghosh, Sanjit A. Seshia, Natarajan Shankar, Ashish Tiwari
TechReport (arXiv) in submission - 2018

Compositional Programming and Testing of Dynamic Distributed Systems

Ankush Desai, Amar Phanishayee, Shaz Qadeer and Sanjit Seshia
International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) - 2018

Programming Safe Robotics Systems: Challenges and Advances

Ankush Desai, Shaz Qadeer and Sanjit Seshia
International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA) - 2018
(invited to the track - A Broader View on Verification: From Static to Runtime and Back)

DRONA: A Framework for Safe Distributed Mobile Robotics

Ankush Desai, Indranil Saha, Jianqiao Yang, Shaz Qadeer and Sanjit Seshia
International Conference on Cyber-Physical Systems (ICCPS) - 2017

Combining Model Checking and Runtime Verification for Safe Robotics

Ankush Desai, Tommaso Dreossi and Sanjit Seshia
The 17th International Conference on Runtime Verification (RV) - 2017

Lasso detection using Partial State Caching

Rashmi Mudduluru, Pantazis Deligiannis, Ankush Desai, Akash Lal and Shaz Qadeer
Formal Methods in Computer-Aided Design (FMCAD) - 2017

Systematic Testing of Asynchronous Reactive Systems

Ankush Desai, Shaz Qadeer and Sanjit Seshia
ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE) - 2015

Approximate Synchrony: An Abstraction for Distributed Almost-synchronous Systems

Ankush Desai, Sanjit Seshia, Shaz Qadeer, David Broman, and John Eidson
International Conference on Computer Aided Verification (CAV) - 2015

Natural proofs for Asynchronous Programs using Almost-synchronous Invariants

Ankush Desai, Pranav Garg, and P. Madhusudan
International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) - 2014

Endlessly Circulating Messages in IEEE 1588-2008 Systems

David Broman, P Derler, Ankush Desai, John Eidson, and Sanjit Seshia
International Symposium on Precision Clock Synchronization for Measurement, Control and Communication (ISPCS) - 2014

P: safe asynchronous event-driven programming

Ankush Desai, Vivek Gupta, Ethan Jackson, Shaz Qadeer, Sriram Rajamani, Damien Zufferey
SIGPLAN conference on Programming Language Design and Implementation (PLDI) - 2013

Depth bounded explicit-state model checking

Abhishek Udupa, Ankush Desai and Sriram Rajamani
International SPIN Symposium on Model Checking of Software (SPIN) - 2011

Tutorials

P: Modular and Safe Asynchronous Programming

Ankush Desai and Shaz Qadeer
The 17th International Conference on Runtime Verification (RV) - 2017 [RV Tutorial]

Workshop papers and Tech. Reports

Formal Specification for Deep Neural Networks

S. A. Seshia, A. Desai, T. Dreossi, D. J. Fremont, S. Ghosh, E. Kim, S. Shivakumar, M. Vazquez- Chanlatte, X. Yue
Technical Report UCB/EECS- 2018-25, EECS Department, University of California, Berkeley - 2018

Iterative Cycle Detection via Delaying Explorers

Ankush Desai, Shaz Qadeer, Sriram Rajamani, and Sanjit Seshia
Microsoft Research Technical Report (MSR-TR-2015-28) - 2015

A New Reduction for Event-Driven Distributed Programs

Ankush Desai, Pranav Garg, and P. Madhusudan
International Workshop on Exploiting Concurrency Efficiently and Correctly (EC2) - 2014

Critical path based performance models for distributed queries

Ankush Desai, Kaushik Rajan, and Kapil Vaswani
Microsoft Research Technical Report (MSR-TR-2012-121) - 2012

Thesis

Design of On Board Computers for a Nanosatellite

Thesis Advisor: Prof. Arnab Bhattacharya
Masters Thesis, IIT, Kanpur - 2010