Projects
P Language
Formal Modeling and Analysis of Distributed Systems
A programming framework for reasoning about correctness of distributed system designs.
P provides a way to model systems as communicating state machines, specify correctness properties,
and systematically test them using model checking and symbolic exploration.
Impact: Used at Microsoft (Windows USB drivers, HoloLens, Azure), AWS (80+ services, 600+ developers),
and DeepSeek (3FS). Detected 300+ bugs in Windows 8 USB driver stack.
Enabled the S3 Strong Consistency launch. Integrated into the development process at AWS.
Drona Framework
Programming Safe Robotics Systems
A framework for building safe distributed mobile robotics systems.
Drona combines formal verification with runtime assurance to provide safety guarantees
for robotics systems that use untrusted components, including machine learning modules.
Impact: Used to program autonomous drone control at UC Berkeley and UPenn (DARPA project).
Extended with the SOTER runtime assurance framework for robotics systems using ML components.
Jugnu Nanosatellite
India's First Nanosatellite (2008–2011)
Led software development for the on-board computer of India's first successful nanosatellite mission.
Designed fault-tolerant software systems for the satellite computer and proposed adaptive communication
protocols for LEO satellites that improved efficiency by 30%.
Impact: Successfully launched on October 12, 2011. Operated for 6 months in space.
Collaboration with ISRO, acknowledged for innovation.