**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.

·
Distributed System Testing and 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.

**Concurren****cy
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.

·
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.

- 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
*.* - 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.