A Parallel Computer Based on Cube-Connected Cycles for Wafer-Scale. - Moon-Jung Chung; Edward J. Toy; Aarti Gupta (FJCC, 1986)

Flexible Parallel Polygon Rendering. - Aarti Gupta; Allan L. Fisher (ICPP (3), 1990)

Formal Hardware Verification Methods: A Survey. - Aarti Gupta (Formal Methods Syst. Des., 1992)

Parametric Circuit Representation Using Inductive Boolean Functions. - Aarti Gupta; Allan L. Fisher (CAV, 1993)

Representation and symbolic manipulation of linearly inductive Boolean functions. - Aarti Gupta; Allan L. Fisher (ICCAD, 1993)

Tradeoffs in Canonical Sequential Function Representations. - Aarti Gupta; Allan L. Fisher (ICCD, 1994)

Toward Formalizing a Validation Methodology Using Simulation Coverage. - Aarti Gupta; Sharad Malik; Pranav Ashar (DAC, 1997)

Integrating a Boolean Satisfiability Checker and BDDs for Combinational Equivalence Checking. - Aarti Gupta; Pranav Ashar (VLSI Design, 1998)

Exploiting Retiming in a Guided Simulation Based Validation Methodology. - Aarti Gupta; Pranav Ashar; Sharad Malik (CHARME, 1999)

Verification of Scheduling in the Presence of Loops Using Uninterpreted Symbolic Simulation. - Pranav Ashar; Anand Raghunathan; Aarti Gupta; Subhrajit Bhattacharya (ICCD, 1999)

SAT-Based Image Computation with Application in Reachability Analysis. - Aarti Gupta; Zijiang Yang 006; Pranav Ashar; Anubhav Gupta 001 (FMCAD, 2000)

Fast Error Diagnosis for Combinational Verification. - Aarti Gupta; Pranav Ashar (VLSI Design, 2000)

Dynamic Detection and Removal of Inactive Clauses in SAT with Application in Image Computation. - Aarti Gupta; Anubhav Gupta 001; Zijiang Yang 006; Pranav Ashar (DAC, 2001)

Property-specific witness graph generation for guided simulation. - Albert E. Casavant; Aarti Gupta; S. Liu; Akira Mukaiyama; Kazutoshi Wakabayashi; Pranav Ashar (DATE, 2001)

Partition-Based Decision Heuristics for Image Computation Using SAT and BDDs. - Aarti Gupta; Zijiang Yang 006; Pranav Ashar; Lintao Zhang; Sharad Malik (ICCAD, 2001)

Using complete-1-distinguishability for FSM equivalence checking. - Pranav Ashar; Aarti Gupta; Sharad Malik (ACM Trans. Design Autom. Electr. Syst., 2001)

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 (DAC, 2002)

Property-Specific Testbench Generation for Guided Simulation. - Aarti Gupta; Albert E. Casavant; Pranav Ashar; Sean Liu; Akira Mukaiyama; Kazutoshi Wakabayashi (ASP-DAC/VLSI Design, 2002)

Assertion-based verification turns the corner. - Aarti Gupta (IEEE Des. Test Comput., 2002)

Abstraction and BDDs Complement SAT-Based BMC in DiVer. - Aarti Gupta; Malay K. Ganai; Chao Wang 001; Zijiang Yang 006; Pranav Ashar (CAV, 2003)

Learning from BDDs in SAT-based bounded model checking. - Aarti Gupta; Malay K. Ganai; Chao Wang 001; Zijiang Yang 006; Pranav Ashar (DAC, 2003)

Iterative Abstraction using SAT-based BMC with Proof Analysis. - Aarti Gupta; Malay K. Ganai; Zijiang Yang 006; Pranav Ashar (ICCAD, 2003)

Efficient Modeling of Embedded Memories in Bounded Model Checking. - Malay K. Ganai; Aarti Gupta; Pranav Ashar (CAV, 2004)

Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. - Malay K. Ganai; Aarti Gupta; Pranav Ashar (ICCAD, 2004)

Verification Languages. - Aarti Gupta; Ali Alphan Bayazit; Yogesh S. Mahajan (The Industrial Information Technology Handbook, 2005)

F-Soft: Software Verification Platform. - Franjo Ivancic; Zijiang Yang 006; Malay K. Ganai; Aarti Gupta; Ilya Shlyakhter; Pranav Ashar (CAV, 2005)

Reasoning About Threads Communicating via Locks. - Vineet Kahlon; Franjo Ivancic; Aarti Gupta (CAV, 2005)

Symmetry Reduction in SAT-Based Model Checking. - Daijue Tang; Sharad Malik; Aarti Gupta; C. Norris Ip (CAV, 2005)

Beyond safety: customized SAT-based model checking. - Malay K. Ganai; Aarti Gupta; Pranav Ashar (DAC, 2005)

Verification of Embedded Memory Systems using Efficient Memory Modeling. - Malay K. Ganai; Aarti Gupta; Pranav Ashar (DATE, 2005)

Model Checking C Programs Using F-SOFT. - Franjo Ivancic; Ilya Shlyakhter; Aarti Gupta; Malay K. Ganai; Vineet Kahlon; Chao Wang 001; Zijiang Yang 006 (ICCD, 2005)

Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination. - Chao Wang 001; Franjo Ivancic; Malay K. Ganai; Aarti Gupta (LPAR, 2005)

DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems. - Malay K. Ganai; Aarti Gupta; Pranav Ashar (TACAS, 2005)

Localization and Register Sharing for Predicate Abstraction. - Himanshu Jain; Franjo Ivancic; Aarti Gupta; Malay K. Ganai (TACAS, 2005)

Lazy Constraints and SAT Heuristics for Proof-Based Abstraction. - Aarti Gupta; Malay K. Ganai; Pranav Ashar (VLSI Design, 2005)

A survey of recent advances in SAT-based formal verification. - Mukul R. Prasad; Armin Biere; Aarti Gupta (Int. J. Softw. Tools Technol. Transf., 2005)

Verification Languages. - Aarti Gupta; Ali Alphan Bayazit; Yogesh S. Mahajan (Embedded Systems Handbook, 2005)

Whodunit? Causal Analysis for Counterexamples. - Chao Wang 001; Zijiang Yang 006; Franjo Ivancic; Aarti Gupta (ATVA, 2006)

Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop. - Himanshu Jain; Franjo Ivancic; Aarti Gupta; Ilya Shlyakhter; Chao Wang 001 (CAV, 2006)

Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions. - Vineet Kahlon; Aarti Gupta; Nishant Sinha 001 (CAV, 2006)

Predicate learning and selective theory deduction for a difference logic solver. - Chao Wang 001; Aarti Gupta; Malay K. Ganai (DAC, 2006)

Disjunctive image computation for embedded software verification. - Chao Wang 001; Zijiang Yang 006; Franjo Ivancic; Aarti Gupta (DATE, 2006)

Accelerating high-level bounded model checking. - Malay K. Ganai; Aarti Gupta (ICCAD, 2006)

An Automata-Theoretic Approach for Model Checking Threads for LTL Propert. - Vineet Kahlon; Aarti Gupta (LICS, 2006)

Mixed symbolic representations for model checking software programs. - Zijiang Yang 006; Chao Wang 001; Aarti Gupta; Franjo Ivancic (MEMOCODE, 2006)

Static Analysis in Disjunctive Numerical Domains. - Sriram Sankaranarayanan 001; Franjo Ivancic; Ilya Shlyakhter; Aarti Gupta (SAS, 2006)

SAT-Based Verification Methods and Applications in Hardware Verification. - Aarti Gupta; Malay K. Ganai; Chao Wang 001 (SFM, 2006)

SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in a Separation Logic Solver. - Malay K. Ganai; Muralidhar Talupur; Aarti Gupta (TACAS, 2006)

Efficient distributed SAT and SAT-based distributed Bounded Model Checking. - Malay K. Ganai; Aarti Gupta; Zijiang Yang 006; Pranav Ashar (Int. J. Softw. Tools Technol. Transf., 2006)

Efficient BMC for Multi-Clock Systems with Clocked Specifications. - Malay K. Ganai; Aarti Gupta (ASP-DAC, 2007)

Fast and Accurate Static Data-Race Detection for Concurrent Programs. - Vineet Kahlon; Yu Yang 013; Sriram Sankaranarayanan 001; Aarti Gupta (CAV, 2007)

Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra. - Chao Wang 001; Zijiang Yang 006; Aarti Gupta; Franjo Ivancic (CAV, 2007)

Induction in CEGAR for Detecting Counterexamples. - Chao Wang 001; Aarti Gupta; Franjo Ivancic (FMCAD, 2007)

From Hardware Verification to Software Verification: Re-use and Re-learn. - Aarti Gupta (Haifa Verification Conference, 2007)

Hybrid CEGAR: combining variable hiding and predicate abstraction. - Chao Wang 001; Hyondeuk Kim; Aarti Gupta (ICCAD, 2007)

Using Ontologies and the Web to Learn Lexical Semantics. - Aarti Gupta; Tim Oates 001 (IJCAI, 2007)

On the analysis of interacting pushdown systems. - Vineet Kahlon; Aarti Gupta (POPL, 2007)

Program Analysis Using Symbolic Ranges. - Sriram Sankaranarayanan 001; Franjo Ivancic; Aarti Gupta (SAS, 2007)

Synthesizing "Verification Aware" Models: Why and How? - Malay K. Ganai; Akira Mukaiyama; Aarti Gupta; Kazutoshi Wakabayashi (VLSI Design, 2007)

SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in Solving Difference Logic. - Malay K. Ganai; Muralidhar Talupur; Aarti Gupta (J. Satisf. Boolean Model. Comput., 2007)

Disjunctive image computation for software verification. - Chao Wang 001; Zijiang Yang 006; Franjo Ivancic; Aarti Gupta (ACM Trans. Design Autom. Electr. Syst., 2007)

SAT-Based Scalable Formal Verification Solutions - Malay K. Ganai; Aarti Gupta (Springer, 2007)

Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions. - Chao Wang 001; Yu Yang 013; Aarti Gupta; Ganesh Gopalakrishnan (ATVA, 2008)

Software Verification: Roles and Challenges for Automatic Decision Procedures. - Aarti Gupta (IJCAR, 2008)

Tunneling and slicing: towards scalable BMC. - Malay K. Ganai; Aarti Gupta (DAC, 2008)

Completeness in SMT-based BMC for Software Programs. - Malay K. Ganai; Aarti Gupta (DATE, 2008)

Mining library specifications using inductive logic programming. - Sriram Sankaranarayanan 001; Franjo Ivancic; Aarti Gupta (ICSE, 2008)

Dynamic inference of likely data preconditions over predicates by tree learning. - Sriram Sankaranarayanan 001; Swarat Chaudhuri; Franjo Ivancic; Aarti Gupta (ISSTA, 2008)

SLR: Path-Sensitive Analysis through Infeasible-Path Detection and Syntactic Language Refinement. - Gogul Balakrishnan; Sriram Sankaranarayanan 001; Franjo Ivancic; Ou Wei; Aarti Gupta (SAS, 2008)

Modular verification of web services using efficient symbolic encoding and summarization. - Fang Yu 001; Chao Wang 001; Aarti Gupta; Tevfik Bultan (SIGSOFT FSE, 2008)

Efficient Modeling of Concurrent Systems in BMC. - Malay K. Ganai; Aarti Gupta (SPIN, 2008)

Peephole Partial Order Reduction. - Chao Wang 001; Zijiang Yang 006; Vineet Kahlon; Aarti Gupta (TACAS, 2008)

Bitwidth Reduction via Symbolic Interval Analysis for Software Model Checking. - Aleksandr Zaks; Zijiang Yang 006; Ilya Shlyakhter; Franjo Ivancic; Srihari Cadambi; Malay K. Ganai; Aarti Gupta; Pranav Ashar (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2008)

Efficient SAT-based bounded model checking for software verification. - Franjo Ivancic; Zijiang Yang 006; Malay K. Ganai; Aarti Gupta; Pranav Ashar (Theor. Comput. Sci., 2008)

Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique. - Vineet Kahlon; Chao Wang 001; Aarti Gupta (CAV, 2009)

Refining the control structure of loops using static analysis. - Gogul Balakrishnan; Sriram Sankaranarayanan 001; Franjo Ivancic; Aarti Gupta (EMSOFT, 2009)

Symbolic Predictive Analysis for Concurrent Programs. - Chao Wang 001; Sudipta Kundu; Malay K. Ganai; Aarti Gupta (FM, 2009)

Robustness of Model-Based Simulations. - Georgios Fainekos; Sriram Sankaranarayanan 001; Franjo Ivancic; Aarti Gupta (RTSS, 2009)

Symbolic pruning of concurrent program executions. - Chao Wang 001; Swarat Chaudhuri; Aarti Gupta; Yu Yang 013 (ESEC/SIGSOFT FSE, 2009)

Semantic Reduction of Thread Interleavings in Concurrent Programs. - Vineet Kahlon; Sriram Sankaranarayanan 001; Aarti Gupta (TACAS, 2009)

Model Checking Concurrent Programs. - Aarti Gupta (VMCAI, 2009)

Preface. - Aarti Gupta; Sharad Malik (Formal Methods Syst. Des., 2009)

Model checking sequential software programs via mixed symbolic analysis. - Zijiang Yang 006; Chao Wang 001; Aarti Gupta; Franjo Ivancic (ACM Trans. Design Autom. Electr. Syst., 2009)

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 001; Nishant Sinha 001; Chao Wang 001 (FMCAD, 2010)

Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. - Sicun Gao; Malay K. Ganai; Franjo Ivancic; Aarti Gupta; Sriram Sankaranarayanan 001; Edmund M. Clarke (FMCAD, 2010)

Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems. - Truong Nghiem; Sriram Sankaranarayanan 001; Georgios Fainekos; Franjo Ivancic; Aarti Gupta; George J. Pappas (HSCC, 2010)

Numerical stability analysis of floating-point computations using software model checking. - Franjo Ivancic; Malay K. Ganai; Sriram Sankaranarayanan 001; Aarti Gupta (MEMOCODE, 2010)

Program analysis via satisfiability modulo path programs. - William R. Harris; Sriram Sankaranarayanan 001; Franjo Ivancic; Aarti Gupta (POPL, 2010)

Trace-Based Symbolic Analysis for Atomicity Violations. - Chao Wang 001; Rhishikesh Limaye; Malay K. Ganai; Aarti Gupta (TACAS, 2010)

Interprocedural Exception Analysis for C++. - Prakash Prabhu; Naoto Maeda; Gogul Balakrishnan; Franjo Ivancic; Aarti Gupta (ECOOP, 2011)

Verifying concurrent programs: tutorial talk. - Aarti Gupta (FMCAD, 2011)

Modeling and Analyzing the Interaction of C and C++ Strings. - Gogul Balakrishnan; Naoto Maeda; Sriram Sankaranarayanan 001; Franjo Ivancic; Aarti Gupta; Rakesh Pothengil (FoVeOOS, 2011)

Predicting Serializability Violations: SMT-Based Search vs. DPOR-Based Search. - Arnab Sinha 001; Sharad Malik; Chao Wang 001; Aarti Gupta (Haifa Verification Conference, 2011)

Coverage guided systematic concurrency testing. - Chao Wang 001; Mahmoud Said; Aarti Gupta (ICSE, 2011)

BEST: A symbolic testing tool for predicting multi-threaded program failures. - Malay K. Ganai; Nipun Arora; Chao Wang 001; Aarti Gupta; Gogul Balakrishnan (ASE, 2011)

DC2: A framework for scalable, scope-bounded software verification. - Franjo Ivancic; Gogul Balakrishnan; Aarti Gupta; Sriram Sankaranarayanan 001; Naoto Maeda; Hiroki Tokuoka; Takashi Imoto; Yoshiaki Miyazaki (ASE, 2011)

Predictive analysis for detecting serializability violations through Trace Segmentation. - Arnab Sinha 001; Sharad Malik; Chao Wang 001; Aarti Gupta (MEMOCODE, 2011)

Symbolic predictive analysis for concurrent programs. - Chao Wang 001; Sudipta Kundu; Rhishikesh Limaye; Malay K. Ganai; Aarti Gupta (Formal Aspects Comput., 2011)

Concurrent Test Generation Using Concolic Multi-trace Analysis. - Niloofar Razavi; Franjo Ivancic; Vineet Kahlon; Aarti Gupta (APLAS, 2012)

Object Model Construction for Inheritance in C++ and Its Applications to Program Analysis. - Jing Yang 003; Gogul Balakrishnan; Naoto Maeda; Franjo Ivancic; Aarti Gupta; Nishant Sinha 001; Sriram Sankaranarayanan 001; Naveen Sharma (CC, 2012)

Symbolic Trajectory Evaluation: The primary validation Vehicle for next generation Intel® Processor Graphics FPU. - V. M. Achutha KiranKumar; Aarti Gupta; Rajnish Ghughal (FMCAD, 2012)

Efficient predictive analysis for detecting nondeterminism in multi-threaded programs. - Arnab Sinha 001; Sharad Malik; Aarti Gupta (FMCAD, 2012)

Efficient Probabilistic Model Checking of Systems with Ranged Probabilities. - Khalil Ghorbal; Parasara Sridhar Duggirala; Vineet Kahlon; Franjo Ivancic; Aarti Gupta (RP, 2012)

DTAM: dynamic taint analysis of multi-threaded programs for relevancy. - Malay K. Ganai; Dongyoon Lee; Aarti Gupta (SIGSOFT FSE, 2012)

Donut Domains: Efficient Non-convex Domains for Abstract Interpretation. - Khalil Ghorbal; Franjo Ivancic; Gogul Balakrishnan; Naoto Maeda; Aarti Gupta (VMCAI, 2012)

Introduction to special section on verification challenges in the concurrent world. - Sandip Ray; Jayanta Bhadra; Magdy S. Abadir; Li-C. Wang; Aarti Gupta (ACM Trans. Design Autom. Electr. Syst., 2012)

Feedback-directed unit test generation for C/C++ using concolic execution. - Pranav Garg 001; Franjo Ivancic; Gogul Balakrishnan; Naoto Maeda; Aarti Gupta (ICSE, 2013)

SETSUDŌ: perturbation-based testing framework for scalable distributed systems. - Pallavi Joshi; Malay K. Ganai; Gogul Balakrishnan; Aarti Gupta; Nadia Papakonstantinou (TRIOS@SOSP, 2013)

Static analysis for concurrent programs with applications to data race detection. - Vineet Kahlon; Sriram Sankaranarayanan 001; Aarti Gupta (Int. J. Softw. Tools Technol. Transf., 2013)

Probabilistic Temporal Logic Falsification of Cyber-Physical Systems. - Houssam Abbas; Georgios Fainekos; Sriram Sankaranarayanan 001; Franjo Ivancic; Aarti Gupta (ACM Trans. Embed. Comput. Syst., 2013)

ReproLite: A Lightweight Tool to Quickly Reproduce Hard System Bugs. - Kaituo Li; Pallavi Joshi; Aarti Gupta; Malay K. Ganai (SoCC, 2014)

An Adaptable Rule Placement for Software-Defined Networks. - Shuyuan Zhang; Franjo Ivancic; Cristian Lumezanu; Yifei Yuan 001; Aarti Gupta; Sharad Malik (DSN, 2014)

Formally Verifying Graphics FPU - An Intel® Experience. - Aarti Gupta; V. M. Achutha KiranKumar; Rajnish Ghughal (FM, 2014)

ARC++: effective typestate and lifetime dependency analysis. - Xusheng Xiao; Gogul Balakrishnan; Franjo Ivancic; Naoto Maeda; Aarti Gupta; Deepak Chhetri (ISSTA, 2014)

Generating consistent updates for software-defined network configurations. - Yifei Yuan 001; Franjo Ivancic; Cristian Lumezanu; Shuyuan Zhang; Aarti Gupta (HotSDN, 2014)

Environment-Sensitive Performance Tuning for Distributed Service Orchestration. - Yu Lin; Franjo Ivancic; Pallavi Joshi; Gogul Balakrishnan; Malay K. Ganai; Aarti Gupta (VECPAR, 2014)

RTL2RTL Formal Equivalence: Boosting the Design Confidence. - M. V. Achutha Kiran Kumar; Aarti Gupta; S. S. Bindumadhava (FSFMA, 2014)

Completeness bounds and sequentialization for model checking of interacting firmware and hardware. - Sunha Ahn; Sharad Malik; Aarti Gupta (CODES+ISSS, 2015)

Assertion guided symbolic execution of multithreaded programs. - Shengjian Guo; Markus Kusano; Chao Wang 001; Zijiang Yang 006; Aarti Gupta (ESEC/SIGSOFT FSE, 2015)

Scalable and scope-bounded software verification in Varvel. - Franjo Ivancic; Gogul Balakrishnan; Aarti Gupta; Sriram Sankaranarayanan 001; Naoto Maeda; Takashi Imoto; Rakesh Pothengil; Mustafa Hussain (Autom. Softw. Eng., 2015)

Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM. - David Menendez; Santosh Nagarakatte; Aarti Gupta (SAS, 2016)

Parallel data race detection for task parallel programs with locks. - Adarsh Yoga; Santosh Nagarakatte; Aarti Gupta (SIGSOFT FSE, 2016)

Trace-based Analysis of Memory Corruption Malware Attacks. - Zhixing Xu; Aarti Gupta; Sharad Malik (Haifa Verification Conference, 2017)

A General Approach to Network Configuration Verification. - Ryan Beckett; Aarti Gupta; Ratul Mahajan; David Walker 001 (SIGCOMM, 2017)

Syntax-Guided Termination Analysis. - Grigory Fedyukovich; Yueling Zhang; Aarti Gupta (CAV (1), 2018)

Exploiting Synchrony and Symmetry in Relational Verification. - Lauren Pick; Grigory Fedyukovich; Aarti Gupta (CAV (1), 2018)

Lazy Self-composition for Security Verification. - Weikun Yang; Yakir Vizel; Pramod Subramanyan; Aarti Gupta; Sharad Malik (CAV (2), 2018)

Formal security verification of concurrent firmware in SoCs using instruction-level abstraction for hardware. - Bo-Yuan Huang 001; Sayak Ray; Aarti Gupta; Jason M. Fung; Sharad Malik (DAC, 2018)

Solving Constrained Horn Clauses Using Syntax and Data. - Grigory Fedyukovich; Sumanth Prabhu 001; Kumar Madhukar; Aarti Gupta (FMCAD, 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 (FMCAD, 2018)

A formal instruction-level GPU model for scalable verification. - Yue Xing 001; Bo-Yuan Huang 001; Aarti Gupta; Sharad Malik (ICCAD, 2018)

PipeProof: Automated Memory Consistency Proofs for Microarchitectural Specifications. - Yatin A. Manerkar; Daniel Lustig; Margaret Martonosi; Aarti Gupta (MICRO, 2018)

Control plane compression. - Ryan Beckett; Aarti Gupta; Ratul Mahajan; David Walker 001 (SIGCOMM, 2018)

Template-Based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification. - Pramod Subramanyan; Bo-Yuan Huang 001; Yakir Vizel; Aarti Gupta; Sharad Malik (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2018)

Model Checking Concurrent Programs. - Aarti Gupta; Vineet Kahlon; Shaz Qadeer; Tayssir Touili (Handbook of Model Checking, 2018)

Quantified Invariants via Syntax-Guided Synthesis. - Grigory Fedyukovich; Sumanth Prabhu 001; Kumar Madhukar; Aarti Gupta (CAV (1), 2019)

Functional Synthesis with Examples. - Grigory Fedyukovich; Aarti Gupta (CP, 2019)

Lemma Synthesis for Automating Induction over Algebraic Data Types. - Weikun Yang; Grigory Fedyukovich; Aarti Gupta (CP, 2019)

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 002; Feng Ye; Tanakorn Leesatapornwongsa; Aarti Gupta; Shan Lu 001; et al. (EuroSys, 2019)

ILAng: A Modeling and Verification Platform for SoCs Using Instruction-Level Abstractions. - Bo-Yuan Huang 001; Hongce Zhang; Aarti Gupta; Sharad Malik (TACAS (1), 2019)

Lazy but Effective Functional Synthesis. - Grigory Fedyukovich; Arie Gurfinkel; Aarti Gupta (VMCAI, 2019)

Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification. - Bo-Yuan Huang 001; Hongce Zhang; Pramod Subramanyan; Yakir Vizel; Aarti Gupta; Sharad Malik (ACM Trans. Design Autom. Electr. Syst., 2019)

Verification of Recurrent Neural Networks for Cognitive Tasks via Reachability Analysis. - Hongce Zhang; Maxwell Shinn; Aarti Gupta; Arie Gurfinkel; Nham Le; Nina Narodytska (ECAI, 2020)

Automating Modular Verification of Secure Information Flow. - Lauren Pick; Grigory Fedyukovich; Aarti Gupta (FMCAD, 2020)

In Search for a SAT-friendly Binarized Neural Network Architecture. - Nina Narodytska; Hongce Zhang; Aarti Gupta; Toby Walsh (ICLR, 2020)

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 (SIGCOMM, 2020)

Fold/Unfold Transformations for Fixpoint Logic. - Naoki Kobayashi 001; Grigory Fedyukovich; Aarti Gupta (TACAS (2), 2020)

Synthesizing Environment Invariants for Modular Hardware Verification. - Hongce Zhang; Weikun Yang; Grigory Fedyukovich; Aarti Gupta; Sharad Malik (VMCAI, 2020)

Abstract interpretation of distributed network control planes. - Ryan Beckett; Aarti Gupta; Ratul Mahajan; David Walker 001 (Proc. ACM Program. Lang., 2020)

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 (CAV (2), 2021)

Leveraging Processor Modeling and Verification for General Hardware Modules. - Yue Xing 001; Huaixi Lu; Aarti Gupta; Sharad Malik (DATE, 2021)

Generating Architecture-Level Abstractions from RTL Designs for Processors and Accelerators Part I: Determining Architectural State Variables. - Yu Zeng; Bo-Yuan Huang 001; Hongce Zhang; Aarti Gupta; Sharad Malik (ICCAD, 2021)

Unbounded Procedure Summaries from Bounded Environments. - Lauren Pick; Grigory Fedyukovich; Aarti Gupta (VMCAI, 2021)

Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking. - Hongce Zhang; Aarti Gupta; Sharad Malik (VMCAI, 2021)

Generalizing Tandem Simulation: Connecting High-level and RTL Simulation Models. - Yue Xing 001; Aarti Gupta; Sharad Malik (ASP-DAC, 2022)

Automatic Generation of Architecture-Level Models from RTL Designs for Processors and Accelerators. - Yu Zeng; Aarti Gupta; Sharad Malik (DATE, 2022)

Error Correction Code Algorithm and Implementation Verification Using Symbolic Representations. - Aarti Gupta; Roope Kaivola; Mihir Parang Mehta; Vaibhav Singh (FMCAD, 2022)

ACORN: Network Control Plane Abstraction using Route Nondeterminism. - Divya Raghunathan; Ryan Beckett; Aarti Gupta; David Walker 001 (FMCAD, 2022)

Usage-Based RTL Subsetting for Hardware Accelerators. - Qinhan Tan; Aarti Gupta; Sharad Malik (ICCAD, 2022)

Compositional Verification Using a Formal Component and Interface Specification. - Yue Xing 001; Huaixi Lu; Aarti Gupta; Sharad Malik (ICCAD, 2022)

Katra: Realtime Verification for Multilayer Networks. - Ryan Beckett; Aarti Gupta (NSDI, 2022)

Specialized Accelerators and Compiler Flows: Replacing Accelerator APIs with a Formal Software/Hardware Interface. - Bo-Yuan Huang 001; Steven Lyubomirsky; Yi Li; Mike He; Thierry Tambe; Gus Henry Smith; Akash Gaonkar; Vishal Canumalla; Gu-Yeon Wei; Aarti Gupta; Zachary Tatlock; Sharad Malik (CoRR, 2022)

High-Level Synthesis for Packet-Processing Pipelines. - Xiangyu Gao; Divya Raghunathan; Ruijie Fang; Tao Wang 088; Xiaotong Zhu; Anirudh Sivaraman; Srinivas Narayana; Aarti Gupta (CoRR, 2022)

CaT: A Solver-Aided Compiler for Packet-Processing Pipelines. - Xiangyu Gao; Divya Raghunathan; Ruijie Fang; Tao Wang 088; Xiaotong Zhu; Anirudh Sivaraman; Srinivas Narayana; Aarti Gupta (ASPLOS (3), 2023)

INVITED: Generalizing the ISA to the ILA: A Software/Hardware Interface for Accelerator-rich Platforms. - Bo-Yuan Huang 001; Hongce Zhang; Aarti Gupta; Sharad Malik (DAC, 2023)

Towards Integrating Formal Methods into ML-Based Systems for Networking. - Fengchen Gong; Divya Raghunathan; Aarti Gupta; Maria Apostolaki (HotNets, 2023)

Combined Scheduling, Memory Allocation and Tensor Replacement for Minimizing Off-Chip Data Accesses of DNN Accelerators. - Yi Li; Aarti Gupta; Sharad Malik (CoRR, 2023)

Psym: Efficient Symbolic Exploration of Distributed Systems. - Lauren Pick; Ankush Desai; Aarti Gupta (Proc. ACM Program. Lang., 2023)

Modular Control Plane Verification via Temporal Invariants. - Timothy Alberdingk Thijm; Ryan Beckett; Aarti Gupta; David Walker 001 (Proc. ACM Program. Lang., 2023)

Synthesizing MILP Constraints for Efficient and Robust Optimization. - Jingbo Wang 006; Aarti Gupta; Chao Wang 001 (Proc. ACM Program. Lang., 2023)

SoC Protocol Implementation Verification Using Instruction-Level Abstraction Specifications. - Huaixi Lu; Yue Xing 001; Aarti Gupta; Sharad Malik (ACM Trans. Design Autom. Electr. Syst., 2023)

Exact Scheduling to Minimize Off-Chip Data Movement for Deep Learning Accelerators. - Yi Li; Aarti Gupta; Sharad Malik (ASPDAC, 2024)

Buffy: A Formal Language-Based Framework for Network Performance Analysis. - Amir Seyhani; Junyi Zhao; Aarti Gupta; David Walker 001; Mina Tahmasbi Arashloo (HotNets, 2024)

Automatic Generation of Cycle-Accurate Timing Models from RTL for Hardware Accelerators. - Yu Zeng; Aarti Gupta; Sharad Malik (ICCAD, 2024)

Zoom2Net: Constrained Network Telemetry Imputation. - Fengchen Gong; Divya Raghunathan; Aarti Gupta; Maria Apostolaki (SIGCOMM, 2024)

Super-resolution on network telemetry time series. - Fengchen Gong; Divya Raghunathan; Aarti Gupta; Maria Apostolaki (CoRR, 2024)

Application-level Validation of Accelerator Designs Using a Formal Software/Hardware Interface. - Bo-Yuan Huang 001; Steven Lyubomirsky; Yi Li; Mike He; Gus Henry Smith; Thierry Tambe; Akash Gaonkar; Vishal Canumalla; Andrew Cheung; Gu-Yeon Wei; Aarti Gupta; Zachary Tatlock; et al. (ACM Trans. Design Autom. Electr. Syst., 2024)

Kirigami, the Verifiable Art of Network Cutting. - Timothy Alberdingk Thijm; Ryan Beckett; Aarti Gupta; David Walker 001 (IEEE/ACM Trans. Netw., 2024)

A Layered Formal Methods Approach to Answering Queue-related Queries. - Divya Raghunathan; Maria Apostolaki; Aarti Gupta (NSDI, 2025)

FLAG: Formal and LLM-assisted SVA Generation for Formal Specifications of On-Chip Communication Protocols. - Yu-An Shih; Annie Lin; Aarti Gupta; Sharad Malik (CoRR, 2025)

Hierarchical Formal Verification of Hardware. - Huaixi Lu; Yue Xing 001; Aarti Gupta; Sharad Malik (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2025)