Aarti Gupta: Publications

Books and Edited Volumes

· Book: M. K. Ganai and A. Gupta: SAT-based Scalable Formal Verification Solutions. Springer, August 2007.

· A. Gupta and D. Kroening, editors: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (SMT '10), July 2010. Edinburgh, Scotland, United Kingdom.

· A. Gupta and S. Malik, editors: Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA. Lecture Notes in Computer Science 5123, Springer, 2008.

· A. Gupta and P. Manolios, editors: Proceedings of the ACM/IEEE Formal Methods in Computer-Aided Design Conference. IEEE, November 2006.

Publications by Topic

· Distributed System Testing and Verification

· Concurrency Verification

· Program Analysis and Verification

· Automatic Decision Procedures

· Verification in Electronic Design Automation

· BDD-based Verification (Ph.D. Thesis research)

· Computer Systems (M.S. Thesis research)

Distributed System Testing and Verification

· K. Li, P. Joshi, A. Gupta, and M. K. Ganai: ReproLite: A Lightweight Tool to Quickly Reproduce Hard System Bugs. In Proceedings of the ACM Symposium on Cloud Computing (SoCC), November 2014.

· S. Park, M. K. Ganai, and A. Gupta: PATRIOT: Runtime Checks for Permission Exploits in the Android System (in submission).

· Y. Lin, F. Ivančić, P. Joshi, G. Balakrishnan, M. K. Ganai, and A. Gupta: Environment-Sensitive Performance Tuning for Distributed Service Orchestration. In the Ninth International Workshop on Automatic Performance Tuning (iWAPT), June 2014.

· Y. Yuan, F. Ivančić, C. Lumezanu, S. Zhang, and A. Gupta: Generating Consistent Updates for Software-Defined Network Configurations. In Proceedings of the ACM SIGCOMM Workshop on Hot Topics in Software Defined Networking (HotSDN), June 2014 (poster paper).

· S. Zhang, F. Ivančić, C. Lumezanu, Y. Yuan, A. Gupta, and S. Malik: An Adaptable Rule Placement for Software-Defined Networks. In Proceedings of the IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), June 2014.

· P. Joshi, M. K. Ganai, G. Balakrishnan, A. Gupta, and N. Papakonstantinou: Setsudo: Perturbation-based Testing Framework for Scalable Distributed Systems. In Proceedings of the Conference on Timely Results in Operating Systems (TRIOS), November 2013.

Concurrency Verification

· A. Gupta, V. Kahlon, S. Qadeer, and T. Touili: Model Checking Concurrent Software. In Handbook of Model Checking, Springer (invited paper, in final review).

· V. Kahlon, S. Sankaranarayanan, and A. Gupta: Static Analysis for Concurrent Programs with Applications to Data Race Detection. Software Tools for Technology Transfer (STTT) 15(4): 321-336, 2013.

· N. Razavi, F. Ivančić, V. Kahlon, and A. Gupta: Concurrent Test Generation using Concolic Multi-Trace Analysis, In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS), December 2012.

· M. K. Ganai, D. Lee, and A. Gupta: DTAM: Dynamic Taint Analysis of Multi-threaded Programs for Relevancy. In ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), November 2012.

· A. Sinha, S. Malik, and A. Gupta: Efficient Predictive Analysis for Detecting Nondeterminism in Multi-threaded Programs. In Proceedings of the International Conference on Computer-Aided Design (FMCAD), October 2012.

· S. Ray, J. Bhadra, M. S. Abadir, L-C. Wang, and A. Gupta: Introduction to Special Section on Verification Challenges in the Concurrent World. ACM Transactions on Design Automation of Electronic Systems 17(3): 19 (2012).

· C. Wang, S. Kundu, R. Limaye, M. K. Ganai, and A. Gupta: Symbolic Predictive Analysis for Concurrent Programs. Formal Aspects of Computing 23(6): 781-805 (2011).

· M. K. Ganai, N. Arora, C. Wang, A. Gupta, and G. Balakrishnan: BEST: A Symbolic Testing Tool for Predicting Multi-threaded Program Failures. In Proceedings of the IEEE/ACM International Conference on Automated Software Engineering (ASE), November 2011.

· A. Sinha, S. Malik, C. Wang, and A. Gupta: Predicting Serializability Violations: SMT-based Search vs. DPOR-based Search, Haifa Verification Conference (HVC), December 2011.

· A. Gupta: Verifying Concurrent Programs: Tutorial Talk. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD), October 2011.

· A. Sinha, S. Malik, C. Wang, and A. Gupta: Predictive Analysis for Detecting Serializability Violations through Trace Segmentation. In Proceedings of the ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), July 2011.

· C. Wang, M. Said, and A. Gupta: Coverage Guided Systematic Concurrency Testing. In Proceedings of the International Conference on Software Engineering (ICSE), May 2011.

· C. Wang, R. Limaye, M. K. Ganai, and A. Gupta: Trace-Based Symbolic Analysis for Atomicity Violations. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), March 2010.

· C. Wang, S. Kundu, M. Ganai, and A. Gupta: Symbolic Predictive Analysis of Concurrent Programs. In Proceedings of the International Symposium on Formal Methods (FM), November 2009.

· C. Wang, S. Chaudhuri, A. Gupta, and Y. Yang: Symbolic Pruning of Concurrent Program Executions. In ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), August 2009.

· V. Kahlon, C. Wang, and A. Gupta: Monotonic Partial Order Reduction. In Proceedings of the International Conference on Computer Aided Verification (CAV), June 2009.

· V. Kahlon, S. Sankaranarayanan, and A. Gupta: Semantic Reduction of Thread Interleavings in Concurrent Programs. In Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), March 2009.

· C. Wang, Y. Yang, A. Gupta, and G. Gopalakrishnan: Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions. In Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis (ATVA), October 2008.

· M. K. Ganai and A. Gupta: Efficient Modeling of Concurrent Systems. In Proceedings of the International SPIN Workshop on Model Checking of Software (SPIN) August 2008.

· C. Wang, Z. Yang, V. Kahlon, and A. Gupta: Peephole Partial Order Reduction. In Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), March 2008.

· V. Kahlon, Y. Yang, S. Sankaranarayanan, and A. Gupta: Fast and Accurate Static Race Detection for Concurrent Programs. In Proceedings of the International Conference on Computer Aided Verification (CAV), July 2007.

· V. Kahlon and A. Gupta: On the Analysis of Interacting Pushdown Systems. In Proceedings of the Conference on Principles of Programming Languages (POPL), January 2007.

· V. Kahlon, N. Sinha, and A. Gupta: Symbolic Model Checking of Concurrent Programs using Partial Orders and On-the-fly Transactions. In Proceedings of the International Conference on Computer Aided Verification (CAV), August 2006.

· V. Kahlon and A. Gupta: An Automata-theoretic Approach for Model Checking Threads for LTL Properties. In Proceedings of the Conference on Logic in Computer Science (LICS), August 2006.

· V. Kahlon, A. Gupta, and F. Ivančić: Reasoning about Threads Communicating via Locks. In Proceedings of the International Conference on Computer Aided Verification (CAV), July 2005.

Program Analysis and Verification

· F. Ivančić, G. Balakrishnan, A. Gupta, S. Sankaranarayanan, N. Maeda, T. Imoto, R. Pothengil, M. Hussain: Scalable and Scope-Bounded Software Verification in Varvel (Accepted for publication in the Journal of Automated Software Engineering, Springer, August 2014.)

· X. Xiao, G. Balakrishan, F. Ivančić, N. Maeda, and A. Gupta: ARC++: Effective Typestate and Lifetime Dependency Analysis. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), July 2014.

· H. Abbas, G. E. Fainekos, S. Sankaranarayanan, F. Ivančić, and A. Gupta: Probabilistic Temporal Logic Falsification of Cyber-Physical Systems. ACM Transactions on Embedded Computing Systems 12(2s): 95, 2013.

· P. Garg, F. Ivančić, G. Balakrishnan, N. Maeda, and A. Gupta: Feedback-Directed Unit Test Generation for C/C++ using Concolic Execution. In Proceedings of the International Conference on Software Engineering (ICSE), May 2013.

· K. Ghorbal, P. S. Duggirala, V. Kahlon, F. Ivančić, and A. Gupta: Efficient Probabilistic Model Checking of Systems with Ranged Probabilities. In the 6^th International Workshop on Reachability Problems (RP), September 2012.

· J. Yang, G. Balakrishnan, N. Maeda, F. Ivančić, A. Gupta, N. Sinha, S. Sankaranarayanan, and N. Sharma: Object Model Construction for Inheritance in C++ and Its Applications to Program Analysis. In Proceedings of International Conference on Compiler Construction (CC), March 2012.

· K. Ghorbal, F. Ivančić, G. Balakrishnan, N. Maeda, and A. Gupta: Donut Domains: Efficient Non-convex Domains for Abstract Interpretation. In Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), January 2012.

· F. Ivančić, G. Balakrishnan, A. Gupta, S. Sankaranarayanan, N. Maeda, H. Tokuoka, T. Imoto, and Y. Miyazaki: DC2: A Framework for Scalable, Scope-Bounded Software Verification. In Proceedings of the IEEE/ACM International Conference on Automated Software Engineering (ASE), November 2011.

· G. Balakrishnan, N. Maeda, S. Sankaranarayanan, F. Ivančić, A. Gupta, and R. Pothengil: Modeling and Analyzing the Interaction of C and C++ Strings. In Proceedings of International Conference on Formal Verification of Object-Oriented Software (FoVeOOS), October 2011.

· P. Prabhu, N. Maeda, G. Balakrishnan, F. Ivančić, and A. Gupta: Interprocedural Exception Analysis for C++. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP), July 2011.

· F. Ivančić, M. K. Ganai, S. Sankaranarayanan, and A. Gupta: Numerical Stability Analysis of Floating-point Computations using Software Model Checking. In Proceedings of the ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), July 2010.

· T. Nghiem, S. Sankaranarayanan, G. E. Fainekos, F. Ivančić, A. Gupta, and G. J. Pappas: Monte-Carlo techniques for falsification of temporal properties of non-linear hybrid systems. In Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control (HSCC), March 2010.

· W. Harris, S. Sankaranarayanan, F. Ivančić, and A. Gupta: Program Analysis via Satisfiability Modulo Path Programs. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL), January 2010.

· G. Fainekos, S. Sankaranarayanan, F. Ivančić, and A. Gupta: Robustness of Model-based Simulations. In Proceedings of the IEEE Real-Time Systems Symposium (RTSS), December 2009.

· G. Balakrishnan, S. Sankaranarayanan, F. Ivančić, and A. Gupta: Refining the Control Structure of Loops using Static Analysis. In Proceedings of the International Conference on Embedded Software (EMSOFT), October 2009.

· Z. Yang, C. Wang, F. Ivančić, and A. Gupta: Model Checking Sequential Software Programs via Mixed Symbolic Analysis. ACM Transactions on Design Automation of Electronic Systems 13(1), January 2009.

· F. Yu, C. Wang, A. Gupta, and T. Bultan: Modular Verification of Web Services using Efficient Symbolic Encoding and Summarization. In Proceedings of the ACM Foundations on Software Engineering (FSE), November 2008.

· F. Ivančić, Z. Yang, M.K. Ganai, A. Gupta, and P. Ashar: Efficient SAT-based Bounded Model Checking for Software Verification. Journal on Theoretical Computer Science (TCS), Volume 404(3), September 2008.

· A. Zaks, Z. Yang, I. Shlyakhter, F. Ivančić, S. Cadambi, M.K. Ganai, A. Gupta, and P. Ashar: Bitwidth Reduction via Symbolic Interval Analysis for Software Model Checking. Transactions Brief Paper in the IEEE Transactions on CAD, volume 27(8), Aug. 2008.

· G. Balakrishnan, S. Sankaranarayanan, F. Ivančić, O. Wei, and A. Gupta: SLR: Path-Sensitive Analysis through Infeasible-Path Detection and Syntactic-Language Refinement. In Proceedings of the Static Analysis Symposium (SAS), July 2008.

· S. Sankaranarayanan, S. Chaudhuri, F. Ivančić, and A. Gupta: Dynamic Inference of Likely Data Preconditions over Predicates by Tree Learning. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), July 2008.

· S. Sankaranarayanan, F. Ivančić and A. Gupta: Mining Library Specifications Using Inductive Logic Programming. In Proceedings of the International Conference on Software Engineering (ICSE), May 2008.

· M. K. Ganai and A. Gupta: Tunneling and Slicing: Towards Scalable BMC. In Proceedings of the IEEE/ACM Design Automation Conference (DAC), June 2008.

M. K. Ganai and A. Gupta: Completeness in SMT-based BMC for Software Programs. In Proceedings of the International Conference of Design, Automation and Test in Europe, March 2008.

· C. Wang, A. Gupta, and F. Ivančić: Induction in CEGAR for Detecting Counterexamples. In Proceedings of the International Conference on Formal Methods in Computer Aided Design (FMCAD), November 2007.

· S. Sankaranarayanan, F. Ivančić, and A. Gupta: Program Analysis using Symbolic Ranges. In Proceedings of the International Static Analysis Symposium (SAS), August 2007.

· C. Wang, Z. Yang, A. Gupta, and F. Ivančić: Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra. In Proceedings of the International Conference on Computer Aided Verification (CAV), July 2007.

· C. Wang, Z. Yang, F. Ivančić, and A. Gupta: Disjunctive Image Computation for Software Verification. ACM Transactions on Design Automation of Electronic Systems 12(2), April 2007. Winner of the ACM TODAES 2008 Best Paper Award.

· C. Wang, Z. Yang, F. Ivančić, and A. Gupta: Whodunit? Causal Analysis for Counterexamples. In Proceedings of the International Symposium on Automated Technology for Verification and Analysis (ATVA), September 2006.

· S. Sankaranarayanan, F. Ivančić, I. Shlyakhter, and A. Gupta: Static Analysis in Disjunctive Numerical Domains. In Proceedings of the International Static Analysis Symposium (SAS), August 2006.

· H. Jain, F. Ivančić, A. Gupta, I. Shlyakhter, and C. Wang: Using Statically Computed Invariants inside the Predicate Abstraction and Refinement Loop, In Proceedings of the International Conference on Computer Aided Verification (CAV), August 2006.

· A. Zaks, I. Shlyakhter, F. Ivančić, S. Cadambi, Z. Yang, M. K. Ganai, A. Gupta, and P. Ashar: Using Range Analysis for Software Verification. In International Workshop on Software Verification and Validation (SVV), August 2006.

· Z. Yang, C. Wang, A. Gupta, and F. Ivančić. Mixed Symbolic Representations for Model Checking Software Programs. In Proceedings of the ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), July 2006.

· C. Wang, Z. Yang, and F. Ivančić, and A. Gupta: Disjunctive Image Computation for Embedded Software Verification. IEEE Design Automation and Test Europe (DATE), March 2006.

F. Ivančić, I. Shlyakhter, M. Ganai, A. Gupta, V. Kahlon, C. Wang, and Z. Yang: Model Checking C Programs using F-Soft. Invited paper in the Proceedings of the IEEE International Conference on Computer Design (ICCD), October 2005.
F. Ivančić, Z. Yang, M. K. Ganai, A. Gupta, I. Shlyakhter, and P. Ashar: F-Soft: Software Verification Platform. In Proceedings of the International Conference on Computer Aided Verification (CAV), July 2005.
H. Jain, F. Ivančić, A. Gupta, and M. K. Ganai: Localization and Register Sharing for Predicate Abstraction. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems (TACAS), April 2005.
F. Ivančić, Z. Yang, M. K. Ganai, A. Gupta, and P. Ashar: Efficient SAT-based Bounded Model Checking for Software Verification, in International Symposium on Leveraging Applications of Formal Methods (ISoLA), November 2004.

Automatic Decision Procedures

· S. Gao, M. K. Ganai, F. Ivančić, A. Gupta, S. Sankaranarayanan, and E. M. Clarke: Integrating ICP and LRA Solvers for Deciding Nonlinear Real Arithmetic Problems. In Proceedings of the International Conference on Formal Methods in Computer Aided Design (FMCAD), October 2010.

· C. Wang, A. Gupta, and M. K. Ganai: Predicate Learning and Selective Theory Deduction for a Difference Logic Solver. In Proceedings of the ACM/IEEE Design Automation Conference (DAC), July 2006.

M. K. Ganai, M. Talupur, and A. Gupta: SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in a Separation Logic Solver. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems (TACAS), March 2006.
C. Wang, F. Ivančić, M. K. Ganai, and A. Gupta: Deciding Separation Logic formulae by SAT and Incremental Negative Cycle Elimination, In Proceedings of International Conference on Logic for Artificial Intelligence and Reasoning (LPAR), December 2005.
M. K. Ganai, L. Zhang, A. Gupta, P. Ashar, and S. Malik: Combining Strengths of Circuit-based and CNF-based Algorithms for a High-performance SAT Solver. In Proceedings of the ACM/IEEE Design Automation Conference (DAC), June 2002.

Verification in Electronic Design Automation

C. Wang, H. Kim, and A. Gupta: Hybrid CEGAR: Combining Variable Hiding and Predicate Abstraction. In Proceedings of the International Conference on Computer Aided Design (ICCAD), November 2007.
M. K. Ganai and A. Gupta: Efficient BMC for Multi-clock Systems with Clocked Specifications. In Proceedings of Asia and South Pacific Design Automation Conference (ASP-DAC), January 2007.
M. K. Ganai, A. Gupta, A. Mukaiyama, and K. Wakabayashi: Synthesizing “Verification Aware” Models: How and Why? In Proceedings of the IEEE VLSI Design Conference, January 2007.
M. K. Ganai and A. Gupta: Accelerating High-level Bounded Model Checking. In Proceedings of the IEEE International Conference on Computer-Aided Design (ICCAD), November 2006.
A. Gupta, M. K. Ganai and C. Wang: SAT-Based Verification Methods and Applications in Hardware Verification. In the International School on Formal Methods for the Design of Computer, Communication and Software Systems: Hardware Verification, Bertinoro, May 2006.
D. Tang, S. Malik, A. Gupta, and C. N. Ip: Symmetry Reduction in SAT-based Model Checking. In Proceedings of International Conference on Computer Aided Verification (CAV), July 2005.
M. K. Ganai, A. Gupta, and P. Ashar: Beyond Safety: Customized SAT-based Model Checking. In Proceedings of the ACM/IEEE Design Automation Conference (DAC), June 2005.
M. K. Ganai, A. Gupta, and P. Ashar: DiVer: SAT-based Model Checking Platform for Large Scale Systems. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems (TACAS), April 2005.
M. K. Ganai, A. Gupta, and P. Ashar: Verification of Embedded Memory Systems using Efficient Memory Modeling. In Proceedings of the IEEE Design Automation and Test Europe (DATE), March 2005.
M. R. Prasad, A. Biere, and A. Gupta: A Survey of Recent Advances in SAT-based Verification. In International Journal on Software Tools for Technology Transfer (STTT), Vol. 7(2):156—173, April 2005.
A. Gupta, M. K. Ganai, and P. Ashar: Lazy Constraints and SAT Heuristics for Proof-based Abstraction. In Proceedings of the IEEE International Conference on VLSI Design, January 2005.
M. K. Ganai, A. Gupta, and P. Ashar: Efficient SAT-based Unbounded Model Checking Using Circuit Cofactoring. In Proceedings of the ACM/IEEE International Conference on Computer-Aided Design (ICCAD), November 2004.

· A. Gupta, A. A. Bayazit, and Y. Mahajan: Verification Languages. Invited article in the “The Industrial Information Technology Handbook”, Ed. R. Zurawski, CRC Press, November 2004.

M. K. Ganai, A. Gupta, and P. Ashar: Efficient Modeling of Embedded Memories in Bounded Model Checking. In Proceedings of the International Conference on Computer Aided Verification (CAV), July 2004.
A. Gupta, M. K. Ganai, Z. Yang, and P. Ashar: Iterative Abstraction using SAT-based BMC with Proof Analysis. In Proceedings of the ACM/IEEE International Conference on Computer-Aided Design (ICCAD), November 2003.
M. K. Ganai, A. Gupta, Z. Yang, and P. Ashar: Efficient Distributed SAT and SAT-based Distributed Bounded Model Checking. In Proceedings of the Conference on Correct Hardware Designs and Verification Methods (CHARME), September 2003.
A. Gupta, C. Wang, M. K. Ganai, Z. Yang, P. Ashar: Abstraction and BDDs Complement SAT-based BMC in DiVer. In Proceedings of the International Conference on Computer Aided Verification (CAV), July 2003.
A. Gupta, M. K. Ganai, C. Wang, Z. Yang, and P. Ashar: Learning from BDDs in SAT-based Bounded Model Checking. In Proceedings of the ACM/IEEE Design Automation Conference (DAC), June 2003.
A. Gupta: Assertion-based Verification Turns the Corner. In IEEE Design & Test of Computers, Volume 19, No. 4, 2002.
A. E. Casavant, A. Gupta, P. Ashar, X. G. Liu, A. Mukaiyama, and K. Wakabayashi: Property-Specific Witness Graph Generation for Guided Simulation. In Proceedings of the IEEE Conference on VLSI Design, January 2002.
A. Gupta, Z. Yang, P. Ashar, L. Zhang, and S. Malik: Partition Based Decision Heuristics for Image Computation Using SAT and BDDs. In Proceedings of the ACM/IEEE International Conference on Computer-Aided Design (ICCAD), Nov. 2001.
P. Ashar, A. Gupta, and S. Malik: Using Complete-1-Distinguishability for FSM equivalence checking. ACM Transactions on Design Automation of Electronic Systems (TODAES), Volume 6 Issue 4, October 2001.
A. Gupta, Anubhav Gupta, Z. Yang, and P. Ashar: Dynamic Detection and Removal of Inactive Clauses in SAT with Application in Image Computation. In Proceedings of the ACM/IEEE Design Automation Conference (DAC), June 2001.
A. Gupta, Z. Yang, P. Ashar, and Anubhav Gupta: SAT-based Image Computation with Application in Reachability Analysis. In Proceedings of the Conference on Formal Methods in Computer-Aided Design (FMCAD), Nov. 2000.
A. Gupta and P. Ashar: Fast Error Diagnosis for Combinational Verification. In Proceedings of the IEEE VLSI Design Conference, January 2000.
P. Ashar, A. Raghunathan, A. Gupta, and S. Bhattacharya: Verification of Scheduling in the Presence of Loops Using Uninterpreted Symbolic Simulation. In Proceedings of the IEEE International Conference on Computer Design (ICCD), October 1999.
A. Gupta, P. Ashar, and S. Malik: Exploiting Retiming in a Guided Simulation Based Validation Methodology. In Proceedings of the Conference on Correct Hardware Design and Verification Methods (CHARME), September 1999.
A. Gupta and P. Ashar: Integrating a Boolean Satisfiability Checker and BDDs for Combinational Verification. In Proceedings of the IEEE VLSI Design Conference, January 1998.
A. Gupta, P. Ashar and S. Malik: Toward Formalizing a Simulation Based Verification Methodology. In Proceedings of the ACM/IEEE Design Automation Conference (DAC), June 1997.
P. Ashar, A. Gupta, and S. Malik: Using Complete-1-Distinguishability for FSM equivalence checking. In Proceedings of the ACM/IEEE International Conference on Computer-Aided Design (ICCAD), June 1996.
A. Gupta: Formal Hardware Verification Methods: A Survey. In Formal Methods in System Design, Kluwer Academic Publishers, Volume 1 (Nos. 2 & 3), October 1992.

BDD-based Verification (related to Ph. D. Thesis)

· Aarti Gupta: Inductive Boolean Function Manipulation: A Hardware Verification Methodology for Automatic Induction, Ph.D. Thesis, Computer Science, Carnegie Mellon University, October 1994.

A. Gupta and A. L. Fisher: Tradeoffs in Canonical Sequential Function Representations. In Proceedings of the IEEE International Conference on Computer Design (ICCD), October 1994. Winner of Outstanding Paper Award.
A. Gupta and A. L. Fisher: Representation and Symbolic Manipulation of Linearly Inductive Boolean Functions. In Proceedings of the ACM/IEEE International Conference on Computer-Aided Design (ICCAD), November 1993.
A. Gupta and A. L. Fisher: Parametric Circuit Representation Using Inductive Boolean Functions. In Proceedings of the International Conference on Computer Aided Verification (CAV), June 1993.

Computer Systems (related to Master’s Thesis)

A. Gupta and A. L. Fisher: Flexible Parallel Polygon Rendering. In Proceedings of the International Conference on Parallel Processing (ICPP), July 1990.
M. J. Chung, E. J. Toy, and A. Gupta. A Highly Parallel Computer in Wafer Scale Integration. In Proceedings of the Conference on VLSI and Computers (CompEuro), July 1987.
M. J. Chung, and E. J. Toy, and A. Gupta: A Parallel Computer based on Cube Connected Cycles for Wafer Scale Integration. In Proceedings of the ACM/IEEE Fall Joint Computer Conference, November 1986.