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

Publications (Google Scholar)

A Runtime Assurance Framework for Programming Safe Robotics Systems

Ankush Desai, Shromona Ghosh, Sanjit A. Seshia, Natarajan Shankar, Ashish Tiwari
IEEE/IFIP International Conference on Dependable Systems and Networks (DSN) - 2019

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