Aarti Gupta: Projects and Related Publications

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

• Psym: Efficient Symbolic Exploration of Distributed Systems.
  Lauren Pick, Ankush Desai, Aarti Gupta.
  In Proceedings of the ACM on Programming Languages Volume 7 (PLDI), 2023.
• Synthesizing MILP Constraints for Efficient and Robust Optimization.
  Jingbo Wang, Aarti Gupta, Chao Wang.
  In Proceedings of the ACM on Programming Languages Volume 7 (PLDI), 2023.
  Distinguished Paper Award
• Pono: A Flexible and Extensible SMT-Based Model Checker.
  Makai Mann, Ahmed Irfan, Florian Lonsing, Yahan Yang, Hongce Zhang, Kristopher Brown, Aarti Gupta, Clark W. Barrett.
  In Proceedings of the International Conference on Computer Aided Verification (CAV), 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.
• Unbounded Procedure Summaries from Bounded Environments. (extended paper with proofs)
  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.
• Fold/Unfold Transformations for Fixpoint Logic.
  Naoki Kobayashi, Grigory Fedyukovich, Aarti Gupta.
  In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2020.
• 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.
• 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.
• Functional Synthesis with Examples.
  Grigory Fedyukovich, Aarti Gupta.
  In Proceedings of the International Conference on Principles and Practice of Constraint Programming (CP) 2019: 547-564.
• 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.
• Lazy but Effective Functional Synthesis.
  Grigory Fedyukovich, Arie Gurfinkel, Aarti Gupta.
  In Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2019: 92-113.
• Solving Constrained Horn Clauses Using Syntax and Data. (pdf)
  Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, Aarti Gupta.
  In Proceedings of the International Conference on Formal Methods in Computer Aided Design, FMCAD 2018.
• Syntax-Guided Termination Analysis. (pdf)
  Grigory Fedyukovich, Yueling Zhang, Aarti Gupta.
  In Proceedings of the International Conference on Computer Aided Verification, CAV (1) 2018: 124-143.
• Exploiting Synchrony and Symmetry in Relational Verification. (pdf)
  Lauren Pick, Grigory Fedyukovich, Aarti Gupta.
  In Proceedings of the International Conference on Computer Aided Verification, CAV (1) 2018: 164-182.
• Lazy Self-composition for Security Verification. (pdf)
  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 and Synthesis

• Modular Control Plane Verification via Temporal Invariants.
  Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, David Walker.
  In Proceedings of the Proceedings of the ACM on Programming Languages, Volume 7 (PLDI), 2023.
• CaT: A Solver-Aided Compiler for Packet-Processing Pipelines.
  Xiangyu Gao, Divya Raghunathan, Ruijie Fang, Tao Wang, Xiaotong Zhu, Anirudh Sivaraman, Srinivas Narayana, Aarti Gupta.
  In Proceedings of the ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3, ASPLOS 2023.
• ACORN: Network Control Plane Abstraction using Route Nondeterminism.
  Divya Raghunathan, Ryan Beckett, Aarti Gupta, David Walker.
  In Proceedings of Formal Methods in Computer-Aided Design (FMCAD), 2023.
• 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.
  Best Paper Award
• Katra: Realtime Verification for Multilayer Networks.
  Ryan Beckett, Aarti Gupta.
  In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation, NSDI 2022.
• 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: 44-61.
• 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. (pdf)
  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. (pdf)
  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 Firmware-Hardware in Systems-on-chip (SoCs)

• INVITED: Generalizing the ISA to the ILA: A Software/Hardware Interface for Accelerator-rich Platforms.
  Bo-Yuan Huang, Hongce Zhang, Aarti Gupta, Sharad Malik.
  In Proceedings of the ACM/IEEE Design Automation Conference (DAC), 2023.
• Generalizing Tandem Simulation: Connecting High-level and RTL Simulation Models.
  Yue Xing, Aarti Gupta, Sharad Malik.
  In Proceedings of the Asia and South Pacific Design Automation Conference (ASPDAC), 2023.
• Compositional Verification Using a Formal Component and Interface Specification.
  Yue Xing, Huaixi Lu, Aarti Gupta, Sharad Malik.
  In Proceedings of the IEEE/ACM International Conference on Computer-Aided Design (ICCAD), 2022.
• Usage-Based RTL Subsetting for Hardware Accelerators.
  Qinhan Tan, Aarti Gupta, Sharad Malik.
  In Proceedings of the IEEE/ACM International Conference on Computer-Aided Design (ICCAD), 2022.
• Automatic Generation of Architecture-Level Models from RTL Designs for Processors and Accelerators.
  Yu Zeng, Aarti Gupta, Sharad Malik.
  In Proceedings of the Design, Automation & Test in Europe Conference (DATE), 2022.
• Generating Architecture-Level Abstractions from RTL Designs for Processors and Accelerators Part I: Determining Architectural State Variables.
  Yu Zeng, Aarti Gupta, Sharad Malik.
  In Proceedings of the IEEE/ACM International Conference on Computer-Aided Design (ICCAD), 2021.
• Leveraging Processor Modeling and Verification for General Hardware Modules.
  Yue Xing, Huaixi Lu, Aarti Gupta, Sharad Malik.
  In Proceedings of the Design Automation and Test in Europe (DATE) Conference, 2021.
  Best Paper Award (Track D)
• 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. (pdf)
  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. (pdf)
  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.
• Formal security verification of concurrent firmware in SoCs using instruction-level abstraction for hardware. (pdf)
  Bo-Yuan Huang, Sayak Ray, Aarti Gupta, Jason M. Fung, Sharad Malik.
  In Proceedings of the 55th Annual Design Automation Conference, DAC 2018: 91:1-91:6.
• Template-Based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification. (pdf)
  Pramod Subramanyan, Bo-Yuan Huang, Yakir Vizel, Aarti Gupta, Sharad Malik.
  IEEE Transactions on CAD of Integrated Circuits and Systems 37(8): 1692-1705 (2018).

Other Recent 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. (pdf)
  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.