Depth Bounded Explicit-State Model Checking. - Abhishek Udupa; Ankush Desai; Sriram K. Rajamani (SPIN, 2011)

P: safe asynchronous event-driven programming. - Ankush Desai; Vivek Gupta; Ethan K. Jackson; Shaz Qadeer; Sriram K. Rajamani; Damien Zufferey (PLDI, 2013)

Natural proofs for asynchronous programs using almost-synchronous reductions. - Ankush Desai; Pranav Garg 001; P. Madhusudan (OOPSLA, 2014)

Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems. - Ankush Desai; Sanjit A. Seshia; Shaz Qadeer; David Broman; John C. Eidson (CAV (2), 2015)

Systematic testing of asynchronous reactive systems. - Ankush Desai; Shaz Qadeer; Sanjit A. Seshia (ESEC/SIGSOFT FSE, 2015)

Lasso detection using partial-state caching. - Rashmi Mudduluru; Pantazis Deligiannis; Ankush Desai; Akash Lal; Shaz Qadeer (FMCAD, 2017)

DRONA: a framework for safe distributed mobile robotics. - Ankush Desai; Indranil Saha; Jianqiao Yang; Shaz Qadeer; Sanjit A. Seshia (ICCPS, 2017)

Combining Model Checking and Runtime Verification for Safe Robotics. - Ankush Desai; Tommaso Dreossi; Sanjit A. Seshia (RV, 2017)

P: Modular and Safe Asynchronous Programming. - Ankush Desai; Shaz Qadeer (RV, 2017)

Formal Specification for Deep Neural Networks. - Sanjit A. Seshia; Ankush Desai; Tommaso Dreossi; Daniel J. Fremont; Shromona Ghosh; Edward Kim 005; Sumukh Shivakumar; Marcell Vazquez-Chanlatte; Xiangyu Yue 001 (ATVA, 2018)

Programming Safe Robotics Systems: Challenges and Advances. - Ankush Desai; Shaz Qadeer; Sanjit A. Seshia (ISoLA (2), 2018)

SOTER: Programming Safe Robotics System using Runtime Assurance. - Ankush Desai; Shromona Ghosh; Sanjit A. Seshia; Natarajan Shankar; Ashish Tiwari 001 (CoRR, 2018)

Compositional programming and testing of dynamic distributed systems. - Ankush Desai; Amar Phanishayee; Shaz Qadeer; Sanjit A. Seshia (Proc. ACM Program. Lang., 2018)

SOTER: A Runtime Assurance Framework for Programming Safe Robotics Systems. - Ankush Desai; Shromona Ghosh; Sanjit A. Seshia; Natarajan Shankar; Ashish Tiwari 001 (DSN, 2019)

SOTER on ROS: A Run-Time Assurance Framework on the Robot Operating System. - Sumukh Shivakumar; Hazem Torfah; Ankush Desai; Sanjit A. Seshia (RV, 2020)

PSec: Programming Secure Distributed Systems using Enclaves. - Shivendra Kushwah; Ankush Desai; Pramod Subramanyan; Sanjit A. Seshia (AsiaCCS, 2021)

Psym: Efficient Symbolic Exploration of Distributed Systems. - Lauren Pick; Ankush Desai; Aarti Gupta (Proc. ACM Program. Lang., 2023)

Message Chains for Distributed System Verification. - Federico Mora 002; Ankush Desai; Elizabeth Polgreen; Sanjit A. Seshia (Proc. ACM Program. Lang., 2023)

Ulgen: A Runtime Assurance Framework for Programming Safe Cyber-Physical Systems. - Beyazit Yalcinkaya; Hazem Torfah; Ankush Desai; Sanjit A. Seshia (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2023)

Systems Correctness Practices at AWS: Leveraging Formal and Semi-formal Methods. - Marc Brooker; Ankush Desai (ACM Queue, 2024)

Checking Observational Correctness of Database Systems Artifact (Troubadour). - Lauren Pick; Amanda Xu; Ankush Desai; Sanjit Seshia; Aws Albarghouthi (Zenodo, 2024)

Checking Observational Correctness of Database Systems. - Lauren Pick; Amanda Xu; Ankush Desai; Sanjit A. Seshia; Aws Albarghouthi (Proc. ACM Program. Lang., 2025)

Systems Correctness Practices at Amazon Web Services. - Marc Brooker; Ankush Desai (Commun. ACM, 2025)