| 2026 | DATE | SecIC3: Customizing IC3 for Hardware Security Verification. | Qinhan Tan, Akash Gaonkar, Yu-Wei Fan, Aarti Gupta, Sharad Malik |
| 2026 | NSDI | Count-Based Abstractions for Performance Verification of Contention Points. | Amir Seyhani, Aarti Gupta, David Walker, Mina Tahmasbi Arashloo |
| 2026 | SP | INSIGHT: Automatic Generation of Explanations for Efficient Identification of Hardware Bugs and Underspecifications. | Vincent Quentin Ulitzsch, Alessandro Bertani, Peter W. Deutsch, David Langus Rodriguez, Kelly Xu, Aarti Gupta, Sharad Malik, Mengjia Yan |
| 2025 | NSDI | A Layered Formal Methods Approach to Answering Queue-related Queries. | Divya Raghunathan, Maria Apostolaki, Aarti Gupta |
| 2024 | ASPDAC | Exact Scheduling to Minimize Off-Chip Data Movement for Deep Learning Accelerators. | Yi Li, Aarti Gupta, Sharad Malik |
| 2024 | HOTNETS | Buffy: A Formal Language-Based Framework for Network Performance Analysis. | Amir Seyhani, Junyi Zhao, Aarti Gupta, David Walker, Mina Tahmasbi Arashloo |
| 2024 | ICCAD | Automatic Generation of Cycle-Accurate Timing Models from RTL for Hardware Accelerators. | Yu Zeng, Aarti Gupta, Sharad Malik |
| 2024 | SIGCOMM | Zoom2Net: Constrained Network Telemetry Imputation. | Fengchen Gong, Divya Raghunathan, Aarti Gupta, Maria Apostolaki |
| 2023 | ASPLOS | 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 |
| 2023 | DAC | INVITED: Generalizing the ISA to the ILA: A Software/Hardware Interface for Accelerator-rich Platforms. | Bo-Yuan Huang, Hongce Zhang, Aarti Gupta, Sharad Malik |
| 2023 | HOTNETS | Towards Integrating Formal Methods into ML-Based Systems for Networking. | Fengchen Gong, Divya Raghunathan, Aarti Gupta, Maria Apostolaki |
| 2022 | ASPDAC | Generalizing Tandem Simulation: Connecting High-level and RTL Simulation Models. | Yue Xing, Aarti Gupta, Sharad Malik |
| 2022 | DATE | Automatic Generation of Architecture-Level Models from RTL Designs for Processors and Accelerators. | Yu Zeng, Aarti Gupta, Sharad Malik |
| 2022 | FMCAD | Error Correction Code Algorithm and Implementation Verification Using Symbolic Representations. | Aarti Gupta, Roope Kaivola, Mihir Parang Mehta, Vaibhav Singh |
| 2022 | FMCAD | ACORN: Network Control Plane Abstraction using Route Nondeterminism. | Divya Raghunathan, Ryan Beckett, Aarti Gupta, David Walker |
| 2022 | ICCAD | Usage-Based RTL Subsetting for Hardware Accelerators. | Qinhan Tan, Aarti Gupta, Sharad Malik |
| 2022 | ICCAD | Compositional Verification Using a Formal Component and Interface Specification. | Yue Xing, Huaixi Lu, Aarti Gupta, Sharad Malik |
| 2022 | ICNP | Kirigami, the Verifiable Art of Network Cutting. | Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, David Walker |
| 2022 | NSDI | Katra: Realtime Verification for Multilayer Networks. | Ryan Beckett, Aarti Gupta |
| 2021 | CAV | 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 |
| 2021 | DATE | Leveraging Processor Modeling and Verification for General Hardware Modules. | Yue Xing, Huaixi Lu, Aarti Gupta, Sharad Malik |
| 2021 | ICCAD | Generating Architecture-Level Abstractions from RTL Designs for Processors and Accelerators Part I: Determining Architectural State Variables. | Yu Zeng, Bo-Yuan Huang, Hongce Zhang, Aarti Gupta, Sharad Malik |
| 2021 | VMCAI | Unbounded Procedure Summaries from Bounded Environments. | Lauren Pick, Grigory Fedyukovich, Aarti Gupta |
| 2021 | VMCAI | Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking. | Hongce Zhang, Aarti Gupta, Sharad Malik |
| 2020 | ECAI | Verification of Recurrent Neural Networks for Cognitive Tasks via Reachability Analysis. | Hongce Zhang, Maxwell Shinn, Aarti Gupta, Arie Gurfinkel, Nham Le, Nina Narodytska |
| 2020 | FMCAD | Automating Modular Verification of Secure Information Flow. | Lauren Pick, Grigory Fedyukovich, Aarti Gupta |
| 2020 | ICLR | In Search for a SAT-friendly Binarized Neural Network Architecture. | Nina Narodytska, Hongce Zhang, Aarti Gupta, Toby Walsh |
| 2020 | SIGCOMM | 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 |
| 2020 | TACAS | Fold/Unfold Transformations for Fixpoint Logic. | Naoki Kobayashi, Grigory Fedyukovich, Aarti Gupta |
| 2020 | VMCAI | Synthesizing Environment Invariants for Modular Hardware Verification. | Hongce Zhang, Weikun Yang, Grigory Fedyukovich, Aarti Gupta, Sharad Malik |
| 2019 | CAV | Quantified Invariants via Syntax-Guided Synthesis. | Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, Aarti Gupta |
| 2019 | CP | Functional Synthesis with Examples. | Grigory Fedyukovich, Aarti Gupta |
| 2019 | CP | Lemma Synthesis for Automating Induction over Algebraic Data Types. | Weikun Yang, Grigory Fedyukovich, Aarti Gupta |
| 2019 | EuroSys | FlyMC: Highly Scalable Testing of Complex Interleavings in Distributed Systems. | Jeffrey F. Lukman, Huan Ke, Cesar A. Stuardo, Riza O. Suminto, Daniar Heri Kurniawan, Dikaimin Simon, Satria Priambada, Chen Tian, Feng Ye, Tanakorn Leesatapornwongsa, Aarti Gupta, Shan Lu, Haryadi S. Gunawi |
| 2019 | TACAS | ILAng: A Modeling and Verification Platform for SoCs Using Instruction-Level Abstractions. | Bo-Yuan Huang, Hongce Zhang, Aarti Gupta, Sharad Malik |
| 2019 | VMCAI | Lazy but Effective Functional Synthesis. | Grigory Fedyukovich, Arie Gurfinkel, Aarti Gupta |
| 2018 | CAV | Syntax-Guided Termination Analysis. | Grigory Fedyukovich, Yueling Zhang, Aarti Gupta |
| 2018 | CAV | Exploiting Synchrony and Symmetry in Relational Verification. | Lauren Pick, Grigory Fedyukovich, Aarti Gupta |
| 2018 | CAV | Lazy Self-composition for Security Verification. | Weikun Yang, Yakir Vizel, Pramod Subramanyan, Aarti Gupta, Sharad Malik |
| 2018 | DAC | Formal security verification of concurrent firmware in SoCs using instruction-level abstraction for hardware. | Bo-Yuan Huang, Sayak Ray, Aarti Gupta, Jason M. Fung, Sharad Malik |
| 2018 | FMCAD | Solving Constrained Horn Clauses Using Syntax and Data. | Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, Aarti Gupta |
| 2018 | FMCAD | 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 |
| 2018 | ICCAD | A formal instruction-level GPU model for scalable verification. | Yue Xing, Bo-Yuan Huang, Aarti Gupta, Sharad Malik |
| 2018 | MICRO | PipeProof: Automated Memory Consistency Proofs for Microarchitectural Specifications. | Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, Aarti Gupta |
| 2018 | SIGCOMM | Control plane compression. | Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker |
| 2017 | SIGCOMM | A General Approach to Network Configuration Verification. | Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker |
| 2016 | SAS | Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM. | David Menendez, Santosh Nagarakatte, Aarti Gupta |
| 2014 | CLOUD | ReproLite: A Lightweight Tool to Quickly Reproduce Hard System Bugs. | Kaituo Li, Pallavi Joshi, Aarti Gupta, Malay K. Ganai |
| 2014 | DSN | An Adaptable Rule Placement for Software-Defined Networks. | Shuyuan Zhang, Franjo Ivancic, Cristian Lumezanu, Yifei Yuan, Aarti Gupta, Sharad Malik |
| 2014 | FM | Formally Verifying Graphics FPU - An Intel Experience. | Aarti Gupta, V. M. Achutha KiranKumar, Rajnish Ghughal |
| 2014 | ISSTA | ARC++: effective typestate and lifetime dependency analysis. | Xusheng Xiao, Gogul Balakrishnan, Franjo Ivancic, Naoto Maeda, Aarti Gupta, Deepak Chhetri |
| 2014 | SIGCOMM | Generating consistent updates for software-defined network configurations. | Yifei Yuan, Franjo Ivancic, Cristian Lumezanu, Shuyuan Zhang, Aarti Gupta |
| 2013 | ICSE | Feedback-directed unit test generation for C/C++ using concolic execution. | Pranav Garg, Franjo Ivancic, Gogul Balakrishnan, Naoto Maeda, Aarti Gupta |
| 2013 | SOSP | SETSUDŌ: perturbation-based testing framework for scalable distributed systems. | Pallavi Joshi, Malay K. Ganai, Gogul Balakrishnan, Aarti Gupta, Nadia Papakonstantinou |
| 2012 | APLAS | Concurrent Test Generation Using Concolic Multi-trace Analysis. | Niloofar Razavi, Franjo Ivancic, Vineet Kahlon, Aarti Gupta |
| 2012 | CC | Object Model Construction for Inheritance in C++ and Its Applications to Program Analysis. | Jing Yang, Gogul Balakrishnan, Naoto Maeda, Franjo Ivancic, Aarti Gupta, Nishant Sinha, Sriram Sankaranarayanan, Naveen Sharma |
| 2012 | FMCAD | Symbolic Trajectory Evaluation: The primary validation Vehicle for next generation Intel Processor Graphics FPU. | V. M. Achutha KiranKumar, Aarti Gupta, Rajnish Ghughal |
| 2012 | FMCAD | Efficient predictive analysis for detecting nondeterminism in multi-threaded programs. | Arnab Sinha, Sharad Malik, Aarti Gupta |
| 2012 | VMCAI | Donut Domains: Efficient Non-convex Domains for Abstract Interpretation. | Khalil Ghorbal, Franjo Ivancic, Gogul Balakrishnan, Naoto Maeda, Aarti Gupta |
| 2011 | ECOOP | Interprocedural Exception Analysis for C++. | Prakash Prabhu, Naoto Maeda, Gogul Balakrishnan, Franjo Ivancic, Aarti Gupta |
| 2011 | FMCAD | Verifying concurrent programs: | Aarti Gupta |
| 2011 | ICSE | Coverage guided systematic concurrency testing. | Chao Wang, Mahmoud Said, Aarti Gupta |
| 2011 | MEMOCODE | Predictive analysis for detecting serializability violations through Trace Segmentation. | Arnab Sinha, Sharad Malik, Chao Wang, Aarti Gupta |
| 2010 | FMCAD | Scalable and precise program analysis at NEC. | Gogul Balakrishnan, Malay K. Ganai, Aarti Gupta, Franjo Ivancic, Vineet Kahlon, Weihong Li, Naoto Maeda, Nadia Papakonstantinou, Sriram Sankaranarayanan, Nishant Sinha, Chao Wang |
| 2010 | FMCAD | Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. | Sicun Gao, Malay K. Ganai, Franjo Ivancic, Aarti Gupta, Sriram Sankaranarayanan, Edmund M. Clarke |
| 2010 | MEMOCODE | Numerical stability analysis of floating-point computations using software model checking. | Franjo Ivancic, Malay K. Ganai, Sriram Sankaranarayanan, Aarti Gupta |
| 2010 | POPL | Program analysis via satisfiability modulo path programs. | William R. Harris, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta |
| 2010 | TACAS | Trace-Based Symbolic Analysis for Atomicity Violations. | Chao Wang, Rhishikesh Limaye, Malay K. Ganai, Aarti Gupta |
| 2009 | CAV | Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique. | Vineet Kahlon, Chao Wang, Aarti Gupta |
| 2009 | EMSOFT | Refining the control structure of loops using static analysis. | Gogul Balakrishnan, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta |
| 2009 | FM | Symbolic Predictive Analysis for Concurrent Programs. | Chao Wang, Sudipta Kundu, Malay K. Ganai, Aarti Gupta |
| 2009 | RTSS | Robustness of Model-Based Simulations. | Georgios Fainekos, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta |
| 2009 | TACAS | Semantic Reduction of Thread Interleavings in Concurrent Programs. | Vineet Kahlon, Sriram Sankaranarayanan, Aarti Gupta |
| 2009 | VMCAI | Model Checking Concurrent Programs. | Aarti Gupta |
| 2008 | ATVA | Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions. | Chao Wang, Yu Yang, Aarti Gupta, Ganesh Gopalakrishnan |
| 2008 | CADE | Software Verification: Roles and Challenges for Automatic Decision Procedures. | Aarti Gupta |
| 2008 | DAC | Tunneling and slicing: towards scalable BMC. | Malay K. Ganai, Aarti Gupta |
| 2008 | DATE | Completeness in SMT-based BMC for Software Programs. | Malay K. Ganai, Aarti Gupta |
| 2008 | ICSE | Mining library specifications using inductive logic programming. | Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta |
| 2008 | ISSTA | Dynamic inference of likely data preconditions over predicates by tree learning. | Sriram Sankaranarayanan, Swarat Chaudhuri, Franjo Ivancic, Aarti Gupta |
| 2008 | SAS | SLR: Path-Sensitive Analysis through Infeasible-Path Detection and Syntactic Language Refinement. | Gogul Balakrishnan, Sriram Sankaranarayanan, Franjo Ivancic, Ou Wei, Aarti Gupta |
| 2008 | TACAS | Peephole Partial Order Reduction. | Chao Wang, Zijiang Yang, Vineet Kahlon, Aarti Gupta |
| 2007 | ASPDAC | Efficient BMC for Multi-Clock Systems with Clocked Specifications. | Malay K. Ganai, Aarti Gupta |
| 2007 | CAV | Fast and Accurate Static Data-Race Detection for Concurrent Programs. | Vineet Kahlon, Yu Yang, Sriram Sankaranarayanan, Aarti Gupta |
| 2007 | CAV | Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra. | Chao Wang, Zijiang Yang, Aarti Gupta, Franjo Ivancic |
| 2007 | FMCAD | Induction in CEGAR for Detecting Counterexamples. | Chao Wang, Aarti Gupta, Franjo Ivancic |
| 2007 | ICCAD | Hybrid CEGAR: combining variable hiding and predicate abstraction. | Chao Wang, Hyondeuk Kim, Aarti Gupta |
| 2007 | IJCAI | Using Ontologies and the Web to Learn Lexical Semantics. | Aarti Gupta, Tim Oates |
| 2007 | POPL | On the analysis of interacting pushdown systems. | Vineet Kahlon, Aarti Gupta |
| 2007 | VLSID | Synthesizing "Verification Aware" Models: Why and How? | Malay K. Ganai, Akira Mukaiyama, Aarti Gupta, Kazutoshi Wakabayashi |
| 2007 | SAS | Program Analysis Using Symbolic Ranges. | Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta |
| 2006 | ATVA | Whodunit? Causal Analysis for Counterexamples. | Chao Wang, Zijiang Yang, Franjo Ivancic, Aarti Gupta |
| 2006 | CAV | Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop. | Himanshu Jain, Franjo Ivancic, Aarti Gupta, Ilya Shlyakhter, Chao Wang |
| 2006 | CAV | Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions. | Vineet Kahlon, Aarti Gupta, Nishant Sinha |
| 2006 | DAC | Predicate learning and selective theory deduction for a difference logic solver. | Chao Wang, Aarti Gupta, Malay K. Ganai |
| 2006 | DATE | Disjunctive image computation for embedded software verification. | Chao Wang, Zijiang Yang, Franjo Ivancic, Aarti Gupta |
| 2006 | ICCAD | Accelerating high-level bounded model checking. | Malay K. Ganai, Aarti Gupta |
| 2006 | LICS | An Automata-Theoretic Approach for Model Checking Threads for LTL Propert. | Vineet Kahlon, Aarti Gupta |
| 2006 | MEMOCODE | Mixed symbolic representations for model checking software programs. | Zijiang Yang, Chao Wang, Aarti Gupta, Franjo Ivancic |
| 2006 | SAS | Static Analysis in Disjunctive Numerical Domains. | Sriram Sankaranarayanan, Franjo Ivancic, Ilya Shlyakhter, Aarti Gupta |
| 2006 | TACAS | Untitled record | Malay K. Ganai, Muralidhar Talupur, Aarti Gupta |
| 2005 | CAV | F-Soft: Software Verification Platform. | Franjo Ivancic, Zijiang Yang, Malay K. Ganai, Aarti Gupta, Ilya Shlyakhter, Pranav Ashar |
| 2005 | CAV | Reasoning About Threads Communicating via Locks. | Vineet Kahlon, Franjo Ivancic, Aarti Gupta |
| 2005 | CAV | Symmetry Reduction in SAT-Based Model Checking. | Daijue Tang, Sharad Malik, Aarti Gupta, C. Norris Ip |
| 2005 | DAC | Beyond safety: customized SAT-based model checking. | Malay K. Ganai, Aarti Gupta, Pranav Ashar |
| 2005 | DATE | Verification of Embedded Memory Systems using Efficient Memory Modeling. | Malay K. Ganai, Aarti Gupta, Pranav Ashar |
| 2005 | ICCD | Model Checking C Programs Using F-SOFT. | Franjo Ivancic, Ilya Shlyakhter, Aarti Gupta, Malay K. Ganai, Vineet Kahlon, Chao Wang, Zijiang Yang |
| 2005 | LPAR | Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination. | Chao Wang, Franjo Ivancic, Malay K. Ganai, Aarti Gupta |
| 2005 | VLSID | Lazy Constraints and SAT Heuristics for Proof-Based Abstraction. | Aarti Gupta, Malay K. Ganai, Pranav Ashar |
| 2005 | TACAS | Untitled record | Malay K. Ganai, Aarti Gupta, Pranav Ashar |
| 2005 | TACAS | Localization and Register Sharing for Predicate Abstraction. | Himanshu Jain, Franjo Ivancic, Aarti Gupta, Malay K. Ganai |
| 2004 | CAV | Efficient Modeling of Embedded Memories in Bounded Model Checking. | Malay K. Ganai, Aarti Gupta, Pranav Ashar |
| 2004 | ICCAD | Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. | Malay K. Ganai, Aarti Gupta, Pranav Ashar |
| 2004 | ISoLA | Efficient SAT-based Bounded Model Checking for Software Verification. | Pranav Ashar, Malay K. Ganai, Aarti Gupta, Franjo Ivancic, Zijiang Yang |
| 2003 | CAV | Abstraction and BDDs Complement SAT-Based BMC in DiVer. | Aarti Gupta, Malay K. Ganai, Chao Wang, Zijiang Yang, Pranav Ashar |
| 2003 | DAC | Learning from BDDs in SAT-based bounded model checking. | Aarti Gupta, Malay K. Ganai, Chao Wang, Zijiang Yang, Pranav Ashar |
| 2003 | ICCAD | Iterative Abstraction using SAT-based BMC with Proof Analysis. | Aarti Gupta, Malay K. Ganai, Zijiang Yang, Pranav Ashar |
| 2002 | DAC | Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver. | Malay K. Ganai, Pranav Ashar, Aarti Gupta, Lintao Zhang, Sharad Malik |
| 2002 | VLSID | Property-Specific Testbench Generation for Guided Simulation. | Aarti Gupta, Albert E. Casavant, Pranav Ashar, Sean Liu, Akira Mukaiyama, Kazutoshi Wakabayashi |
| 2001 | DAC | Dynamic Detection and Removal of Inactive Clauses in SAT with Application in Image Computation. | Aarti Gupta, Anubhav Gupta, Zijiang Yang, Pranav Ashar |
| 2001 | DATE | Property-specific witness graph generation for guided simulation. | Albert E. Casavant, Aarti Gupta, S. Liu, Akira Mukaiyama, Kazutoshi Wakabayashi, Pranav Ashar |
| 2001 | ICCAD | Partition-Based Decision Heuristics for Image Computation Using SAT and BDDs. | Aarti Gupta, Zijiang Yang, Pranav Ashar, Lintao Zhang, Sharad Malik |
| 2000 | FMCAD | SAT-Based Image Computation with Application in Reachability Analysis. | Aarti Gupta, Zijiang Yang, Pranav Ashar, Anubhav Gupta |
| 2000 | VLSID | Fast Error Diagnosis for Combinational Verification. | Aarti Gupta, Pranav Ashar |
| 1999 | ICCD | Verification of Scheduling in the Presence of Loops Using Uninterpreted Symbolic Simulation. | Pranav Ashar, Anand Raghunathan, Aarti Gupta, Subhrajit Bhattacharya |
| 1998 | VLSID | Integrating a Boolean Satisfiability Checker and BDDs for Combinational Equivalence Checking. | Aarti Gupta, Pranav Ashar |
| 1997 | DAC | Toward Formalizing a Validation Methodology Using Simulation Coverage. | Aarti Gupta, Sharad Malik, Pranav Ashar |
| 1996 | ICCAD | Using complete-1-distinguishability for FSM equivalence checking. | Pranav Ashar, Aarti Gupta, Sharad Malik |
| 1994 | ICCD | Tradeoffs in Canonical Sequential Function Representations. | Aarti Gupta, Allan L. Fisher |
| 1993 | CAV | Parametric Circuit Representation Using Inductive Boolean Functions. | Aarti Gupta, Allan L. Fisher |
| 1993 | ICCAD | Representation and symbolic manipulation of linearly inductive Boolean functions. | Aarti Gupta, Allan L. Fisher |
| 1990 | ICPP | Flexible Parallel Polygon Rendering. | Aarti Gupta, Allan L. Fisher |