About

Madhusudan Parthasarathy is a professor at the Siebel School of Computing and Data Science at the University of Illinois Urbana-Champaign. He earned his Ph.D. in Theoretical Computer Science from the Institute of Mathematical Sciences, University of Madras, Chennai, India, in 2002. His research has significantly impacted the field of formal language theory, particularly through the definition of visibly pushdown languages, a formal language class that has influenced academia and practical applications such as XML processing, program verification, and programming languages. His research interests include reasoning with heaps in software verification, software verification, reliable and secure software engineering, security, program synthesis, and logic and automata theory.

Selected publications

• A Customized Fusion of RF and XGB for Enhanced Malicious URL Detection

  Lecture notes in networks and systems · 2025-01-01

  book-chapter
  PublisherDOI

• Synthesizing DSLs for Few-Shot Learning

  Proceedings of the ACM on Programming Languages · 2025-10-09 · 1 citations

  articleOpen accessSenior author

  We study the problem of synthesizing domain-specific languages (DSLs) for few-shot learning in symbolic domains. Given a base language and instances of few-shot learning problems, where each instance is split into training and testing samples, the DSL synthesis problem asks for a grammar over the base language that guarantees that small expressions solving training samples also solve corresponding testing samples. We prove that the problem is decidable for a class of languages whose semantics over fixed structures can be evaluated by tree automata and when expression size corresponds to parse tree depth in the grammar, and, furthermore, the grammars solving the problem correspond to a regular set of trees. We also prove decidability results for variants of the problem where DSLs are only required to express solutions for input learning problems and where DSLs are defined using macro grammars.

  PublisherDOI

• FO-Complete Program Verification for Heap Logics

  Proceedings of the ACM on Programming Languages · 2025-04-09

  articleOpen accessSenior author

  Program verification techniques for expressive heap logics are inevitably incomplete. In this work we argue that algorithmic techniques for reasoning with expressive heap logics can be held up to a different robust theoretical standard for completeness: FO-Completeness. FO-completeness is a theoretical guarantee that all theorems that are valid when recursive definitions are interpreted as fixpoint definitions (instead of least fixpoint) are guaranteed to be eventually proven by the system. We illustrate a set of principles to design such logics and develop the first two heap logics that have implicit heaplets and that admit FO-Complete program verification. The logics we develop are a frame logic (FL) and a separation logic (SL-FL) that has an alternate semantics inspired by frame logic. We show a verification condition generation technique that is amenable to FO-complete reasoning using quantifier instantiation and SMT solvers. We implement tools that realize our technique and show the expressiveness of our logics and the efficacy of the verification technique on a suite of benchmarks that manipulate data structures.

  PublisherDOI

• Frame Logic Verifier Tool from "FO-Complete Program Verification for Heap Logics"

  Artifact Digital Object Group · 2025-04-09 · 1 citations

  datasetSenior author
  PublisherDOI

• Predictable Verification using Intrinsic Definitions

  Proceedings of the ACM on Programming Languages · 2024-06-20 · 2 citations

  preprintOpen accessSenior author

  We propose a novel mechanism of defining data structures using intrinsic definitions that avoids recursion and instead utilizes monadic maps satisfying local conditions. We show that intrinsic definitions are a powerful mechanism that can capture a variety of data structures naturally. We show that they also enable a predictable verification methodology that allows engineers to write ghost code to update monadic maps and perform verification using reduction to decidable logics. We evaluate our methodology using B oogie and prove a suite of data structure manipulating programs correct.

  PublisherOA PDFDOI

• ConjunCT: Learning Inductive Invariants to Prove Unbounded Instruction Safety Against Microarchitectural Timing Attacks

  2024-05-19 · 7 citations

  article

  The past decade has seen a deluge of microarchitectural side channels stemming from a variety of hardware structures (the cache, branch predictor, execution ports, the TLB, speculation, etc). These attacks stem from software that passes sensitive data to so-called unsafe or transmitter instructions, i.e., those whose execution time depends on their operands’ values. Correspondingly, there has been a large number of defenses (spanning hardware and software) that attempt to enforce the policy: sensitive data ↛ unsafe instruction operand. Implementing this policy assumes that one can identify unsafe instructions for a given microarchitecture. But this is quite difficult—requiring the designer to analyze potentially unbounded compositions of dynamic instructions to tease out subtle interactions they may have with one another.This paper addresses the above challenge by proposing ConjunCT. Given RTL: ConjunCT proves, for all possible executions, whether each ISA instruction is either i) safe for an unbounded number of cycles or ii) unsafe. This is done using a combination of symbolic analysis (to generate examples) and inductive invariant learning (bootstrapped by said examples), and enabled by a novel conditional information flow predicate that we show is useful for analyzing information flows in processor pipelines.We demonstrate our analysis on several RISC-V microarchitectures of varying complexity, and use it to extract the safe/unsafe sets for each. Through a judicious use of program synthesis, we are able to automate the analysis (almost entirely) from end to end, e.g., requiring only 8 designer annotations to fully analyze the RISC-V RocketChip core. Lastly, we show through several case studies how ConjunCT can be used by microarchitects to understand the security implications of an advanced optimization, and how the invariants generated by ConjunCT can be used to localize where in the microarchitecture unsafety occurs.

  PublisherDOI

• Perception Contracts for Safety of ML-Enabled Systems

  Proceedings of the ACM on Programming Languages · 2023-10-16 · 15 citations

  articleOpen access

  We introduce a novel notion of perception contracts to reason about the safety of controllers that interact with an environment using neural perception. Perception contracts capture errors in ground-truth estimations that preserve invariants when systems act upon them. We develop a theory of perception contracts and design symbolic learning algorithms for synthesizing them from a finite set of images. We implement our algorithms and evaluate synthesized perception contracts for two realistic vision-based control systems, a lane tracking system for an electric vehicle and an agricultural robot that follows crop rows. Our evaluation shows that our approach is effective in synthesizing perception contracts and generalizes well when evaluated over test images obtained during runtime monitoring of the systems.

  PublisherOA PDFDOI

• Complete First-Order Reasoning for Properties of Functional Programs

  Proceedings of the ACM on Programming Languages · 2023-10-16 · 3 citations

  articleOpen accessSenior author

  Several practical tools for automatically verifying functional programs (e.g., Liquid Haskell and Leon for Scala programs) rely on a heuristic based on unrolling recursive function definitions followed by quantifier-free reasoning using SMT solvers. We uncover foundational theoretical properties of this heuristic, revealing that it can be generalized and formalized as a technique that is in fact complete for reasoning with combined First-Order theories of algebraic datatypes and background theories, where background theories support decidable quantifier-free reasoning. The theory developed in this paper explains the efficacy of these heuristics when they succeed, explain why they fail when they fail, and the precise role that user help plays in making proofs succeed.

  PublisherOA PDFDOI

• A First-order Logic with Frames

  ACM Transactions on Programming Languages and Systems · 2023-02-09 · 3 citations

  articleOpen accessSenior author

  We propose a novel logic, Frame Logic (FL), that extends first-order logic and recursive definitions with a construct Sp (·) that captures the implicit supports of formulas—the precise subset of the universe upon which their meaning depends. Using such supports, we formulate proof rules that facilitate frame reasoning elegantly when the underlying model undergoes change. We show that the logic is expressive by capturing several data-structures and also exhibit a translation from a precise fragment of separation logic to frame logic. Finally, we design a program logic based on frame logic for reasoning with programs that dynamically update heaps that facilitates local specifications and frame reasoning. This program logic consists of both localized proof rules as well as rules that derive the weakest tightest preconditions in frame logic.

  PublisherOA PDFDOI

• Languages with Decidable Learning: A Meta-theorem

  Proceedings of the ACM on Programming Languages · 2023-04-06 · 4 citations

  articleOpen accessSenior author

  We study expression learning problems with syntactic restrictions and introduce the class of finite-aspect checkable languages to characterize symbolic languages that admit decidable learning. The semantics of such languages can be defined using a bounded amount of auxiliary information that is independent of expression size but depends on a fixed structure over which evaluation occurs. We introduce a generic programming language for writing programs that evaluate expression syntax trees, and we give a meta-theorem that connects such programs for finite-aspect checkable languages to finite tree automata, which allows us to derive new decidable learning results and decision procedures for several expression learning problems by writing programs in the programming language.

  PublisherOA PDFDOI

Awards & honors

• ACM Europe Council Best Paper Award at PLDI '24