Mukund Raghothaman

Department of Computer and Information Science
University of Pennsylvania
3330 Walnut St GRW 571
Philadelphia, PA 19104


Research Interests

Formal verification and program synthesis. Automata theory and model checking.





  1. Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo Martin, Mukund Raghothaman, Sanjit Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. Syntax-guided synthesis. In Formal Methods in Computer-Aided Design (FMCAD), pages 1--17, 2013. [Paper].
  2. Rajeev Alur, Loris D’Antoni, Jyotirmoy V. Deshmukh, Mukund Raghothaman, and Yifei Yuan. Regular functions and cost register automata. Symposium on Logic in Computer Science, pages 13--22, 2013. [Paper], [Full version].
  3. Rajeev Alur and Mukund Raghothaman. Decision problems for additive regular functions. In Fedor Fomin, Rūsiņš Freivalds, Marta Kwiatkowska, and David Peleg, editors, Automata, Languages, and Programming, volume 7966 of Lecture Notes in Computer Science, pages 37--48. Springer, 2013. [Paper], [Full version], [Slides].
  4. Rajeev Alur, Adam Freilich, and Mukund Raghothaman. Regular combinators for string transformations. In Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, pages 9:1--9:10. ACM, 2014. [Paper], [Full version], [Slides].
  5. Rajeev Alur, Milo Martin, Mukund Raghothaman, Christos Stergiou, Stavros Tripakis, and Abhishek Udupa. Synthesizing finite-state protocols from scenarios and requirements. In 10th International Haifa Verification Conference (To appear in), HVC ’14, 2014.
  6. Rajeev Alur, Loris D’Antoni, Mukund Raghothaman. DReX: A Declarative Language for Efficiently Evaluating Regular String Transformations. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’15, pages 125--137. ACM, 2015. [Paper], [Full paper], [PRECISE Industry Day, 2014, 2-minute pitch slides], [POPL 2015 Slides], [DReX Webpage], [Implementation].

Technical Reports

  1. Mukund Raghothaman. Learning techniques in verification and model checking. Written Preliminary Exam — 2, Available at [Paper], [Slides], 2012.


  1. While in college, I was involved with the IITG amateur astronomy club. Having grown up in a city, I barely know my way around the night sky without a sky chart. But I did help with organizing some competitions — mostly with framing (hopefully interesting) questions. Here are two problem sets, from 2009, and from 2010. There was also a “design” competition in 2010, with a more open-ended task.