Aarti Gupta

Aarti Gupta is a Professor in the Department of Computer Science at Princeton University, where she conducts research in formal verification, program analysis, and automated decision procedures. She has made significant contributions to the field of system analysis and verification, with her work being applied in industrial settings. Before joining Princeton, she led research in systems analysis and verification at NEC Labs America.

Dr. Gupta received her PhD in Computer Science from Carnegie Mellon University. Her academic journey has positioned her as a leading figure in formal methods and verification techniques.

Her research focuses on two main areas: theoretical foundations and practical applications. Foundations include formal methods, model checking, program analysis, automated synthesis, and SAT/SMT solvers. Applications span verification of software, hardware, networks, and distributed systems. Gupta's work bridges the gap between theoretical advances and real-world implementation, with particular emphasis on developing techniques that scale to handle complex industrial systems.

Gupta's recent publications demonstrate a clear trajectory toward more modular, scalable, and practical verification techniques. She has increasingly focused on network verification, with several papers addressing the challenges of verifying distributed network control planes. Her work also shows growing interest in hardware verification, particularly for Systems-on-Chip (SoCs), and the intersection of formal methods with neural networks. A notable trend is the development of techniques that combine symbolic reasoning with learning approaches to improve verification scalability.

Dr. Gupta has received numerous prestigious awards for her contributions:

• ACM Fellow (2017) - for contributions to system analysis and verification techniques and their transfer to industrial practice
• PLDI 2023 Distinguished Paper Award for "Synthesizing MILP Constraints for Efficient and Robust Optimization"
• IEEE ICNP 2022 Best Paper Award
• DATE 2021 Best Paper Award (Track D)
• ACM TODAES 2020 Best Paper Award
• IEEE Micro Top Pick 2018 Honorable Mention

Dr. Gupta has advised numerous graduate students and postdoctoral researchers, including current PhD candidates Divya Raghunathan, Akash Gaonkar, Deyuan He, and Dexin Zhang. Among her former students are Timothy Alberdingk Thijm and Lauren Pick. She has also mentored postdoctoral fellow Grigory Fedyukovich and visiting student Yueling Zhang. Her research has been supported by significant grants that have enabled her to lead projects such as SyLVer (Synthesis, Learning, and Verification) and network verification initiatives in collaboration with researchers like Dave Walker and Ryan Beckett.

Dr. Gupta leads the SyLVer research group at Princeton, which focuses on developing techniques that improve the scalability of algorithmic verification by combining deductive learning with learning on data and examples. Her group collaborates extensively on network verification projects, particularly through the Minesweeper initiative with Dave Walker and Ryan Beckett, and on Instruction Level Abstraction (ILA) for System-on-Chip verification in collaboration with Sharad Malik's group.