Kimaya Bedarkar

About

I am Kimaya Bedarkar, a final-year PhD student at MPI-SWS and Saarland University, jointly supervised by Björn Brandenburg, Derek Dreyer, and Deepak Garg.

I did my bachelor’s and master’s at BITS Pilani, then moved to Germany for an internship with Björn at MPI-SWS. After the internship, I stayed on for a PhD. In summer 2024, I interned with the RiSE team at Microsoft Research, where I worked on verifying parts of production C code using AI agents and formal verification tools.

My research brings together real-time systems and program verification. I started out mechanizing schedulability analyses in Rocq as part of Prosa, proving that scheduling policies provide the timing guarantees we expect. From there, I moved on to connecting those proofs to concrete scheduler implementations in RefinedProsa (PLDI 2025). More recently, in my RTSS 2026 work, I’ve been deploying and running these systems on commodity hardware, connecting formal timing guarantees to their runtime behavior.

Looking ahead, I’m excited about making formal verification practical for large-scale production systems by combining formal methods with AI. Drawing on my experience with separation logic-based verification, I’m particularly interested in building verification tools and abstractions that AI agents can use effectively.

Outside of work, I enjoy riding my bike and watching movies.