Aarti Gupta: Projects and Selected Publications

Formal Methods with and for Machine Learning

There has been an explosion of interest in using Artificial Intelligence (AI) agents and Large Language Models (LLMs) in software and systems development. I am interested in combining them with techniques for formal methods (FM) and programming languages (PL) for enhancing correctness, safety, and performance.

Selected Publications

• Soteria: Formally Verified Planning with Runtime Enforcement for Safe LLM Agents.
  Deyuan He, Ankush Desai, Sharad Malik, Aarti Gupta.
  NeurIPS 2026 (accepted as Oral).
  
• Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification.
  Zenan Li, Ziran Yang, Mike He, Haoyu Zhao, A. Zhao, Shange Tang, Kaiyu Yang, Aarti Gupta, Zhendong Su, Chi Jin.
  COLM 2026.
  
• SVAEval: An Evaluation Framework for LLM-based SVA Property Generators.
  Yu-An Shih, Soohyuk Cho, Aarti Gupta and Sharad Malik.
  In proceedings of FMCAD 2026.
  
• ALGOVERI: An Aligned Benchmark for Verified Code Generation on Classical Algorithms.
  Haoyu Zhao, Ziran Yang, Jiawei Li, Deyuan He, Zenan Li, Chi Jin, Venugopal V. Veeravalli, Aarti Gupta, Sanjeev Arora.
  ICML 2026, ICML spotlight paper.
• Position: The Case for Theory-Level Autoformalization.
  Marcus J. Min, Mike He, Zhaoyu Li, Zixuan Yi, Sharad Malik, Aarti Gupta, Xujie Si, Osbert Bastani.
  ICML 2026, ICML spotlight position track paper.
  
• Ranking Formal Specifications using LLMs.
  Mike He, Zhendong Ang, Ankush Desai, and Aarti Gupta.
  In Proceedings of the 1st ACM SIGPLAN International Workshop on Language Models and Programming Languages (LMPL), 2025.
  

SyLVer: Synthesis, Learning, and Verification

Algorithmic verification techniques have made tremendous progress by leveraging advancements in decision procedures based on SAT/SMT solvers. The project aims to develop techniques that improve their scalability for program verification and synthesis, by combining deductive learning with learning on data and examples. The targeted applications include:

• Automatic generation of invariants for program verification
• Verification of program security

Selected Publications

• Specy: Learning Specifications for Distributed Systems from Event Traces.
  Deyuan He, Ankush Desai, Aishwarya Jagarapu, Doug Terry, Sharad Malik, Aarti Gupta.
  In Proceedings of the International Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2026), ACM PACMPL Symposium, 2026.
  
• Qinhan Tan, Akash Gaonkar, Yu-Wei Fan, Aarti Gupta and Sharad Malik.
  SecIC3: Customizing IC3 for Hardware Security Verification.
  In Proceedings of the Design Automation and Test in Europe Conference (DATE), 2026.
  Nominated for Best Paper Award.
• Psym: Efficient Symbolic Exploration of Distributed Systems.
  Lauren Pick, Ankush Desai, Aarti Gupta.
  ACM International Conference on Programming Language Design and Implementation (PLDI), 2023.
  
• Unbounded Procedure Summaries from Bounded Environments.
  Lauren Pick, Grigory Fedyukovich, Aarti Gupta.
  In Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2021.
• Automating modular verification of secure information flow.
  Lauren Pick, Grigory Fedyukovich, Aarti Gupta.
  In Proceedings of the International Conference on Formal Methods in Computer Aided Design (FMCAD), 2020.
• Quantified Invariants via Syntax-Guided Synthesis.
  Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, Aarti Gupta.
  In Proceedings of the International Conference on Computer Aided Verification, CAV 2019.
• Lemma Synthesis for Automating Induction over Algebraic Data Types.
  Weikun Yang, Grigory Fedyukovich, Aarti Gupta.
  In Proceedings of the International Conference on Principles and Practice of Constraint Programming (CP) 2019: 600-617.
• Syntax-Guided Termination Analysis.
  Grigory Fedyukovich, Yueling Zhang, Aarti Gupta.
  In Proceedings of the International Conference on Computer Aided Verification, CAV (1) 2018.
  
• Lazy Self-composition for Security Verification.
  Weikun Yang, Yakir Vizel, Pramod Subramanyan, Aarti Gupta, Sharad Malik.
  In Proceedings of the International Conference on Computer Aided Verification, CAV (2) 2018: 136-156.

Network Verification

Networks form an essential component of the computing infrastructure that interconnects the world and provides immensely useful products and services in modern society. As the design complexity of networks continues to grow, there has been great interest in applying formal verification techniques on computer networks, to provide guarantees of correctness for properties of interest.

Selected Publications

• CB-VER: A Stable Foundation for Modular Network Control Plane Verification.
  Dexin Zhang, Timothy Alberdingk Thijm, David Walker and Aarti Gupta.
  In Proceedings of FMCAD 2026.
• Count-Based Abstractions for Performance Verification of Contention Points.
  Amir Seyhani, Aarti Gupta, David Walker, Mina Tahmasbi Arashloo.
  In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2026
  
• A Layered Formal Methods Approach to Answering Queue-related Queries.
  Divya Raghunathan, Maria Apostolaki, and Aarti Gupta.
  In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2025
  
• Zoom2Net: Constrained Network Telemetry Imputation.
  Fengchen Gong, Divya Raghunathan, Maria Apostolaki, and Aarti Gupta.
  In Proceedings of SIGCOMM, 2024.
  
• Towards Integrating Formal Methods into ML-Based Systems for Networking.
  Fengchen Gong, Divya Raghunathan, Aarti Gupta, Maria Apostolaki.
  In Proceedings of HotNets 2023.
  
• Modular Control Plane Verification via Temporal Invariants.
  Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, David Walker.
  ACM International Conference on Programming Language Design and Implementation (PLDI), 2023.
  
• Optimizing Compilers for Packet-Processing Pipelines.
  Xiangyu Gao, Divya Raghunathan, Ruijie Fang, Tao Wang, Xiaotong Zhu, Anirudh Sivaraman, Srinivas Narayana, Aarti Gupta.
  ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2023.
  
• ACORN: Network Control Plane Abstraction using Route Nondeterminism.
  Divya Raghunathan, Ryan Beckett, Aarti Gupta, David Walker.
  In Proceedings of FMCAD, 2022.
  
• Kirigami, the Verifiable Art of Network Cutting.
  Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, David Walker.
  In Proceedings of the IEEE International Conference on Network Protocols (ICNP), 2022.
  Winner of the Best Paper Award.
• Switch Code Generation Using Program Synthesis.
  Xiangyu Gao, Taegyun Kim, Michael D. Wong, Divya Raghunathan, Aatish Kishan Varma, Pravein Govindan Kannan, Anirudh Sivaraman, Srinivas Narayana, Aarti Gupta.
  In Proceedings of SIGCOMM 2020.
  

Minesweeper: in collaboration with Dave Walker and Ryan Beckett

• Abstract interpretation of distributed network control planes.
  Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker.
  In Proceedings of the ACM on Programming Languages, 4(POPL): 42:1-42:27 (2020).
• Control Plane Compression. Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker.
  In Proceedings of the Conference of the ACM Special Interest Group on Data Communication, SIGCOMM 2018: 476-489.
• A General Approach to Network Configuration Verification. Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker.
  In Proceedings of the Conference of the ACM Special Interest Group on Data Communication, SIGCOMM 2017: 155-168.

Verification of Hardware and Firmware in Systems-on-chip (SoCs)

An ILA is a formal specification and abstraction for processors, accelerators, and general hardware. It captures their software-visible functionality, using the familiar notion of computation triggered by “instructions” (similar to an Instruction Set Architecture, ISA, for processors). Top-down an ILA model provides a specification for functional verification of hardware, and bottom-up it provides an abstraction with operational semantics for software/hardware co-verification.

Selected Publications

• Hierarchical Formal Verification of Hardware.
  Huaixi Lu, Yue Xing, Aarti Gupta, Sharad Malik.
  IEEE Transactions on Computer Aided Design and Integrated Circuits and Systems, 44(9), 2025.
  
• Application-level Validation of Accelerator Designs Using a Formal Software/Hardware Interface.
  Bo-Yuan Huang, Steven Lyubomirsky, Yi Li, Mike He, Gus Henry Smith, Thierry Tambe, Akash Gaonkar, Vishal Canumalla, Andrew Cheung, Gu-Yeon Wei, Aarti Gupta, Zachary Tatlock, Sharad Malik.
  ACM Transactions on Design Automation of Electronic Systems 29(2): 35:1-35:25 (2024).
  
• SoC Protocol Implementation Verification Using Instruction-Level Abstraction Specifications.
  Huaixi Lu, Yue Xing, Aarti Gupta, Sharad Malik.
  ACM Transactions on Design Automation of Electronic Systems 28(6), 2023.
  
• Compositional Verification Using a Formal Component and Interface Specification.
  Yue Xing, Huaixi Lu, Aarti Gupta, Sharad Malik.
  IEEE/ACM International Conference on Computer Aided Design (ICCAD), 2022.
  
• Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking.
  Hongce Zhang, Aarti Gupta, Sharad Malik.
  In Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2021.
• Synthesizing Environment Invariants for Modular Hardware Verification.
  Hongce Zhang, Weikun Yang, Grigory Fedyukovich, Aarti Gupta, Sharad Malik.
  In Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2020.
• Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification.
  Bo-Yuan Huang, Hongce Zhang, Pramod Subramanyan, Yakir Vizel, Aarti Gupta, Sharad Malik.
  ACM Transactions on Design Automation of Electronic Systems 24(1): 10:1-10:24 (2019).
  ACM TODAES Best Paper Award 2020.
  
• ILAng: A Modeling and Verification Platform for SoCs Using Instruction-Level Abstractions.
  Bo-Yuan Huang, Hongce Zhang, Aarti Gupta, Sharad Malik.
  In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS (1) 2019: 351-357.
• A Formal Instruction-Level GPU Model for Scalable Verification.
  Yue Xing, Bo-Yuan Huang, Aarti Gupta, Sharad Malik.
  In Proceedings of the International Conference on Computer-Aided Design, ICCAD 2018.
• ILA-MCM: Integrating Memory Consistency Models with Instruction-Level Abstractions for Heterogeneous System-on-Chip Verification. Hongce Zhang, Caroline Trippel, Yatin A. Manerkar, Aarti Gupta, Margaret Martonosi, Sharad Malik.
  In Proceedings of the International Conference on Formal Methods in Computer Aided Design, FMCAD 2018.

Other Publications

• Verification of Recurrent Neural Networks for Cognitive Tasks via Reachability Analysis.
  Hongce Zhang, Maxwell Shinn, Aarti Gupta, Arie Gurfinkel, Nham Le, Nina Narodytska.
  In Proceedings of the European Conference on Artificial Intelligence (ECAI), 2020.
• In Search for a SAT-Friendly Binarized Neural Network Architecture.
  Nina Narodytska, Hongce Zhang, Aarti Gupta, Toby Walsh.
  In Proceedings of the International Conference on Learning Representations (ICLR), 2020.
• Automated Memory Consistency Proofs for Microarchitectural Specifications. Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, and Aarti Gupta.
  In Proceedings of the 51st Annual IEEE/ACM International Symposium on Microarchitecture (MICRO), October 2018.
  Nominated for best paper, IEEE Micro Top Pick 2018 Honorable Mention.
• Model Checking Concurrent Programs.
  Aarti Gupta, Vineet Kahlon, Shaz Qadeer, Tayssir Touili.
  In the Handbook of Model Checking, Springer, 2018: 573-611.