Ankush Desai

I am a Senior Applied Scientist in the Database Services (DBS) group at AWS. I am currently working on applying formal method techniques to reason about the correctness of distributed services across AWS (S3, DBS, EBS, ..). These techniques range from lightweight automated approaches like model checking, to systematic testing, to more rigorous deductive verification that provide mathematical proofs. My goal is to integrate the principles of formal methods in all the phases of development process from system design, to implementation, to unit and integration testing, and even in production. Helping service teams across AWS to deliver services with higher assurance of correctness.

Before joining the DBS group, I was part of the S3 team and worked on the Amazon S3's Strong Consistency project (Pi-Week Talk). I am one of the creators and the lead developer of the P programming framework.

I graduated with a PhD in computer science from UC, Berkeley (2019). I was extremely fortunate to be co-advised by Prof. Sanjit Seshia and Dr. Shaz Qadeer. Before joining graduate school, I had the privilege of spending 2+ years working at Microsoft Research, India with Sriram Rajamani. During my time at IIT, Kanpur, I extremely was lucky to be a part of the team that built the first Indian Nano-Satellite JUGNU and had lots of (fun -- Pictures). The satellite was successfully launched on 12 October, 2011 . I was head of the On-Board Computers team managing all the software framework for the satellite.

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.