Publications

Full list also available on Google Scholar.

Conference & Journal Papers

2026
• Feedback-guided Adaptive Testing of Distributed Systems Designs
  Ao Li, Ankush Desai, Rohan Padhye
  USENIX Symposium on Networked Systems Design and Implementation (NSDI) — 2026
  Paper
• Specy: Learning Specifications for Distributed Systems from Event Traces
  Mike He, Ankush Desai, Aishwarya Jagarapu, Doug Terry, Sharad Malik, Aarti Gupta
  Proceedings of the ACM on Programming Languages (OOPSLA) — 2026 (to appear)
• Trace-Guided Synthesis of Effectful Test Generators
  Zhe Zhou, Ankush Desai, Benjamin Delaware, Suresh Jagannathan
  arXiv preprint — 2026
  Paper
2025
• Ranking Formal Specifications using LLMs
  Mike He, Zhendong Ang, Ankush Desai, Aarti Gupta
  Proceedings of the 1st ACM SIGPLAN International Workshop on Language Models and Programming Languages (LMPL) — 2025
  Paper
• Checking Observational Correctness of Database Systems
  Lauren Pick, Amanda Xu, Ankush Desai, Sanjit A. Seshia, Aws Albarghouthi
  Proceedings of the ACM on Programming Languages, Vol. 9, No. OOPSLA1 (OOPSLA) — April 2025
  Paper
• Systems Correctness Practices at Amazon Web Services
  Marc Brooker, Ankush Desai
  Communications of the ACM, Vol. 68, No. 6 — June 2025
  CACM Paper ACM Queue (2024)
2023
• Message Chains for Distributed System Verification
  Federico Mora, Ankush Desai, Elizabeth Polgreen, Sanjit A. Seshia
  Proceedings of the ACM on Programming Languages, Vol. 7, No. OOPSLA2 (OOPSLA) — October 2023
  Paper
• Psym: Efficient Symbolic Exploration of Distributed Systems
  Lauren Pick, Ankush Desai, Aarti Gupta
  Proceedings of the ACM on Programming Languages, Vol. 7, No. PLDI (PLDI) — June 2023
  Paper
• Ulgen: A Runtime Assurance Framework for Programming Safe Cyber-Physical Systems
  Beyazit Yalcinkaya, Hazem Torfah, Ankush Desai, Sanjit A. Seshia
  IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), Vol. 42, No. 11 — November 2023
  Paper
2021
• PSec: Programming Secure Distributed Systems using Enclaves
  Shivendra Kushwah, Ankush Desai, Pramod Subramanyan, Sanjit Seshia
  ACM Asia Conference on Computer and Communications Security (AsiaCCS) — 2021
  Paper
2020
• A Run-Time Assurance Framework on the Robot Operating System
  Sumukh Shivakumar, Hazem Torfah, Ankush Desai, Sanjit A. Seshia
  International Conference on Runtime Verification (RV) — 2020
  Paper
2019
• SOTER: 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
  Paper
2018
• Compositional Programming and Testing of Dynamic Distributed Systems
  Ankush Desai, Amar Phanishayee, Shaz Qadeer, Sanjit Seshia
  International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) — 2018
  Paper TechReport P GitHub
• Programming Safe Robotics Systems: Challenges and Advances
  Ankush Desai, Shaz Qadeer, Sanjit Seshia
  International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA) — 2018
  Paper
2017
• DRONA: A Framework for Safe Distributed Mobile Robotics
  Ankush Desai, Indranil Saha, Jianqiao Yang, Shaz Qadeer, Sanjit Seshia
  International Conference on Cyber-Physical Systems (ICCPS) — 2017
  Paper Drona Webpage
• Combining Model Checking and Runtime Verification for Safe Robotics
  Ankush Desai, Tommaso Dreossi, Sanjit Seshia
  The 17th International Conference on Runtime Verification (RV) — 2017
  Paper Drona Webpage
• Lasso Detection using Partial State Caching
  Rashmi Mudduluru, Pantazis Deligiannis, Ankush Desai, Akash Lal, Shaz Qadeer
  Formal Methods in Computer-Aided Design (FMCAD) — 2017
  Paper
2015
• Systematic Testing of Asynchronous Reactive Systems
  Ankush Desai, Shaz Qadeer, Sanjit Seshia
  ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE) — 2015
  Paper
• Approximate Synchrony: An Abstraction for Distributed Almost-synchronous Systems
  Ankush Desai, Sanjit Seshia, Shaz Qadeer, David Broman, John Eidson
  International Conference on Computer Aided Verification (CAV) — 2015
  Paper TechReport
2014
• Natural Proofs for Asynchronous Programs using Almost-synchronous Invariants
  Ankush Desai, Pranav Garg, P. Madhusudan
  International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) — 2014
  Paper
• Endlessly Circulating Messages in IEEE 1588-2008 Systems
  David Broman, P. Derler, Ankush Desai, John Eidson, Sanjit Seshia
  International Symposium on Precision Clock Synchronization for Measurement, Control and Communication (ISPCS) — 2014
  Paper
2013
• 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
  Paper P GitHub
2011
• Depth Bounded Explicit-State Model Checking
  Abhishek Udupa, Ankush Desai, Sriram Rajamani
  International SPIN Symposium on Model Checking of Software (SPIN) — 2011
  Paper
2010
• Jugnu: Student Nanosatellite from Indian Institute of Technology, Kanpur
  Jugnu Team
  Indian Small Satellite Systems Conference (ISSSC) at ISRO Satellite Center, India — 2010

Tutorials

• P: Modular and Safe Asynchronous Programming
  Ankush Desai, Shaz Qadeer
  The 17th International Conference on Runtime Verification (RV) — 2017 [RV Tutorial]

Workshop Papers & Technical 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, University of California, Berkeley — 2018
  Paper
• Iterative Cycle Detection via Delaying Explorers
  Ankush Desai, Shaz Qadeer, Sriram Rajamani, Sanjit Seshia
  Microsoft Research Technical Report (MSR-TR-2015-28) — 2015
  Paper Zing Model Checker
• A New Reduction for Event-Driven Distributed Programs
  Ankush Desai, Pranav Garg, P. Madhusudan
  International Workshop on Exploiting Concurrency Efficiently and Correctly (EC2) — 2014
  Paper
• Critical Path Based Performance Models for Distributed Queries
  Ankush Desai, Kaushik Rajan, Kapil Vaswani
  Microsoft Research Technical Report (MSR-TR-2012-121) — 2012
  Paper

Thesis

• Modular and Safe Event-Driven Programming
  Advisors: Prof. Sanjit Seshia and Dr. Shaz Qadeer
  PhD Thesis, EECS, UC Berkeley — 2019
  Thesis
• Design of On Board Computers for a Nanosatellite
  Advisor: Prof. Arnab Bhattacharya
  Masters Thesis, IIT Kanpur
  Thesis