Aarti Gupta

My research interests are in Formal Methods (FM) and logic-based reasoning for programs, networks, systems, and hardware. I'm also interested in integration of FM with Artificial Intelligence (AI) and Machine Learning (ML). I am currently serving on the Steering Committee of the International Conference on Computer Aided Verification (CAV). I received a PhD in Computer Science from Carnegie Mellon University.

Before joining the CS Department at Princeton, I was at NEC Labs America where I led research in systems analysis and verification. At NEC, my group and I designed techniques for verifying programs, and helped in their successful deployment on large industrial software projects.

Research Interests

• Foundations: formal methods, model checking, program analysis, automated synthesis, SAT/SMT solvers
• Applications: verification of software, hardware, networks, distributed systems

Recent Awards

• DATE (Design, Automation, and Test in Europe) 2026: Nomination for Best Paper Award
• ACM Conference on Programming Language Design and Implementation (PLDI) 2023: Distinguished Paper Award
• IIT Delhi Distinguished Alumni Award 2023
• IEEE International Conference on Network Protocols (ICNP) 2022: Best Paper Award
• Design, Automation, and Test in Europe (DATE) 2021: Best Paper Award (Track D)
• ACM Transactions on Design Automation of Electronic Systems 2020: Best Paper Award
• IEEE Micro Top Pick 2018: Honorable Mention (also nominated for Best Paper at MICRO-51 conference)
• ACM Fellow: 2017 (for contributions to system analysis and verification techniques and their transfer to industrial practice)

Recent Invited Talks

• Invited keynote talk at the ATVA Conference, October 2025: Network Abstractions for Modularity and Performance Verification.
• Distinguished Lecture in Computer Science Series, Barnard College, October 2023: Ensuring Network Correctness: Scaling Automated Verification.
• Invited talk at the Workshop on Hyperproperties: Advances in Theory and Practice, July 2023: Secure information flow: Lazy self-decomposition and Modular verification.
• Invited Keynote at the Federated Logic Conferences (FLoC), August 2022: SMT-based Verification of Distributed Network Control Planes.
• Bryant Discoveries Day at FLoC, August 2022: BDD (R)evolution: Extending Across Generations.
• Invited talk at the Indian Association for Research in Computing Science (IARCS) Verification Series, June 2022: Formal Verification of Distributed Network Control Planes.
• Invited talk at the Cambridge Isaac Newton Institute Workshop on Verified Software: From Theory to Practice, May 2021: Abstract Interpretation of Distributed Network Control Planes.
• Invited Keynote at the 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT), July 2020: With a little help from structured friends
• Invited talk at the 11th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), July 2019: Verifying Network Control Planes
• Invited talk, The Best of Model Checking: Workshop in honor of Orna Grumberg, July 2019: Abstractions due to Symmetry in Network Control Planes
• Invited Tutorial at the Third SAT+SMT School (India), December 2018: Automated Verification of Programs and Networks using SAT/SMT

Projects and Related Publications

• Formal Methods with and for AI and Machine Learning: in collaboration with Profs. Chi Jin, Sharad Malik (Princeton), Osbert Bastani (Univ of Pennsylvania), Xujie Si (Univ of Toronto)
• SyLVer: Synthesis, Learning, and Verification
• Network Verification: in collaboration with Profs. Maria Apostolaki and Dave Walker (Princeton)
• Instruction Level Abstraction (ILA) for Hardware Verification: in collaboration with Prof. Sharad Malik (Princeton)

Group

• Graduate Students
  • Akash Gaonkar
  • Deyuan He
  • Dexin Zhang
  • Sean Wang
  • Paul Jiang
• Graduated Students
  • Divya Raghunathan (Graduated February 2025, now at AWS)
  • Timothy Alberdingk Thijm (Graduated February 2024, now at Apple)
  • Lauren Pick (Graduated November 2021, now Assistant Professor at CUHK)
• Post-Doctoral Fellows
  • Grigory Fedyukovich: October 2017 -- August 2019

Publications

On the DBLP server

Teaching

• Fall 2026: COS Independent Work (IW) Seminar -- Auto-generation of Programs, Specifications, and Proofs
• Spring 2026: COS 598B (Advanced Topics in Computer Science) -- Formal methods with and for Machine Learning
• Spring 2025, Fall 2025: COS Independent Work (IW) Seminar -- Auto-generation of Programs, Specifications, and Tests
• Fall 2024, Fall 2023, Fall 2020, Fall 2019: COS 516 / ELE 516 -- Automated Reasoning about Software
• Spring 2024: COS 598A (Advanced Topics in Computer Science) -- Verification and Synthesis
• Spring 2022, Spring 2017, Spring 2016, Spring 2015: COS 217 -- Introduction to Programming Systems
• Fall 2021: COS 326 -- Functional Programming
• Spring 2021: COS IW05 (Independent Work Seminar) -- Programs Generating Programs
• Spring 2020: COS 598B (Advanced Topics in Computer Science) -- Advances in Automated Reasoning
• Fall 2018, Spring 2019: COS IW09 (Independent Work Seminar) -- Programs Generating Programs
• Spring 2018: COS 598A (Advanced Topics in Computer Science) -- Advances in Verification
• Fall 2017, Fall 2016: COS 516 / ELE 516 -- Automated Reasoning about Software
• Fall 2015: COS 597B (Advanced Topics in Computer Science) -- Automated Reasoning about Software