Madhusudan Parthasarathy

(217) 244-1323

3226 Siebel Center for Comp Sci

For More Information

2002 Ph.D., Theoretical Computer Science, Institute of Mathematical Sciences, University of Madras, Chennai, India.

Defined a formal language class called visibly pushdown languages (also called nested word languages. This has had a tremendous impact in academia (see Wikipedia page entries: https://en.wikipedia.org/wiki/Nested_word ). This has not just been widely cited, but has defined a new model that people have extensively studied (see http://scholar.google.com/scholar?as_q=&as_oq=%22nested+words%22+%22visibly+pushdown%22 for a Google Scholar search for "nested words" OR "visibly pushdown" that lists more than 940 entries). The class of visibly pushdown languages is an insertion into the Chomsky hierarchy, falling between regular languages and deterministic context-free languages, but which possesses most closure properties that regular languages have while yet remaining tractable. In particular, the inclusion problem is decidable and this has led to applications ranging from XML processing to program verification to programming languages.

Reasoning with heaps in software verification (Natural proofs, Strand, separation logic);
Software Verification; Reliable and secure software engineering; Security; Program Synthesis; Logic and Automata Theory.

Faria Kalim, Karl Palmskog, Jayasi Mehar, Adithya Murali, Indranil Gupta, P. Madhusudan. "Kaizen: Building a Verified and Performant Blockchain System." Proceedings of Formal Methods in Computer-Aided Design (FMCAD), 2019.
Umang Mathur, P. Madhusudan, and Mahesh Viswanathan. "Decidable verification of uninterpreted programs." Proceedings of the ACM on Programming Languages 3, no. POPL (2019): 46.
Angello Astorga,, P. Madhusudan, Shambwaditya Saha, Shiyu Wang, and Tao Xie. "Learning stateful preconditions modulo a test generator." In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 775-787. ACM, 2019.
Christof Loding, P. Madhusudan, and Lucas Pena. Foundations for natural proofs and quantifier instantiation. Proc. ACM Principles of Programming Languages, POPL 2018, Article 10, 30 pages.
S. Bandhakavi, S. King, P. Madhusudan, M. Winslett. VEX: Vetting Browser Extensions For Security Vulnerabilities. Proc. of 19th USENIX Security Symposium, Washington, DC, USA, 2010, USENIX. (Acc rate:14.8%) Won the Best Paper Award
R. Alur and P. Madhusudan. "Visibly Pushdown Languages." In Proc. Symp. on Theory of Computing (STOC), pp. 202-211, Chicago, 2004. (Acc rate: 25.8%)

Visited Microsoft Research, India during sabbatical (2012-2013). Helped initiate a very large MOOC platform for India, called MASSIVELY EMPOWERED CLASSROOMS. This massive online classroom setting is a unique blended classroom meant for undergraduate students in India. Undergraduate colleges in India have a huge quality problem. The blended classroom allows tens of thousands of students in India to access quality lectures and class material that is synchronized with their study. Huge grassroots movement to engage teachers, involve them in the platform, incentivize colleges to participate, and certificate program to incentivize students to take the course to get jobs. Organized and partially lectured the first course on the platform as well. The program has been a huge success with a large number of courses and tens of thousands of undergraduate students each semester.