NEC Laboratories America, Inc.
Aarti Gupta
NEC Laboratories America, Inc.
(609)
951-2966
Email:
agupta at nec-labs dot com
____________________________________________
Research Interests
- Software Systems Analysis and Verification: software model checking, program verification, static analyzers, dynamic verification, formal methods
- Formal Verification: model checking, abstraction-refinement techniques, equivalence checking, hardware verification
- Constraint solvers: Boolean satisfiability (SAT) solvers, Binary Decision Diagrams (BDDs), Satisfiability Modulo Theory (SMT) solvers
- Electronic Design Automation: specification and verification languages, semi-formal verification, simulation-based validation
Recent Professional Activities
- Co-Chair for the International
Conference on Computer Aided Verification (CAV 2008)
- PC Member and
Conference Organization
- FMCAD 2008,
HVC 2008, TACAS 2009
- Done: Co-Chair for Formal
Methods in Computer Aided Design (FMCAD
2006)
- Done: CAV 2008, SAT 2008,
TACAS 2008, FSTTCS 2007, FMCAD 2007, ATVA 2007, HVC 2007, SMT 2007, SAT
2007, DATE 2007, FMCAD 2006, BMC 2006, SVV 2006, DATE 2006
- Associate Editor for Formal Methods in System Design, Springer
- Associate Editor for ACM Transactions on Design Automation
of Electronic Systems (TODAES)
Invited Talks
- VMCAI 2009: Model
Checking Concurrent Multi-threaded Programs
- IJCAR 2008: Software Verification: Roles and Challenges for Automatic Decision Procedures
- HVC 2007: From
Hardware Verification to Software Verification: Re-use and Re-learn
- IBM IRL Workshop 2006: Enhancing Model Checking with Static
Code Analysis for Verifying Programs
- SSPV 2006:
Verifying C Programs using SAT-based model
checking
- SFM 2006: SAT-based Hardware Verification
Publications
Concurrent Program Verification
- M. K. Ganai and A. Gupta. Efficient
Modeling of Concurrent Systems. 15th
International SPIN Workshop on Model Checking of Software (SPIN)
- 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, A. Gupta, and N.
Sinha. 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 IEEE Symposium on Logic in Computer Science (LICS),
August 2006.
- V. Kahlon,
F. Ivancic, A. Gupta. Reasoning about threads communicating via locks,
in Proceedings of the International Conference on Computer Aided
Verification (CAV), July 2005.
Program Verification
- G. Balakrishnan, S. Sankaranarayanan, F. Ivancic, O. Wei, and A. Gupta, SLR: Path-Sensitive Analysis Through Infeasible-Path Detection and Syntactic-Language Refinement. In Proc. Static Analysis Symposium (SAS), July 2008.
- Sriram Sankaranarayanan, Swarat
Chaudhuri, Franjo Ivancic, and Aarti Gupta: Dynamic Inference of Likely
Data Preconditions over Predicates by Tree Learning. (ISSTA), July 2008.
- Sriram Sankaranarayanan, Franjo
Ivancic, and Aarti Gupta: Mining Library Specifications Using Inductive
Logic Programming, Intl. Conference on Software Engg. (ICSE), May 2008.
- M. K. Ganai and A. Gupta,
Tunneling and Slicing: Towards Scalable BMC, in Proc. Design Automation Coference (DAC),
- C. Wang, A. Gupta, and F.
Ivancic. Induction in CEGAR for Detecting Counterexamples. In
Proceedings of the International Conference on Formal Methods in Computer
Aided Design (FMCAD), November 2007.
- F. Ivancic, Z. Yang, M.K.
Ganai, A. Gupta, and P. Ashar. Efficient SAT-based Bounded Model
Checking for Software Verification. In Journal on
Theoretical Computer Science (TCS), accepted
for publication.
- S. Sankaranarayanan, F.
Ivancic, 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. Ivancic.
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. Ivancic,
and A. Gupta.
Disjunctive Image Computation for Software Verification.
In ACM Trans. on Design Automation of Electronic
Systems. 12(2):10, April 2007.
- C. Wang, Z. Yang, F. Ivancic,
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.
Ivancic,
- A. Zaks,
- H. Jain, F. Ivancic,
- Z. Yang, C. Wang, A. Gupta, and
F. Ivancic.
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, F. Ivancic
and A. Gupta.
Disjunctive image computation for embedded software
verification (with). IEEE Design
Automation and Test
- F. Ivancic,
- F-Soft:
Software verification platform (with F. Ivancic, Z. Yang, M. K. Ganai, I. Shlyakhter,
and P. Ashar). In Proceedings of the International Conference on Computer Aided
Verification (CAV), July 2005.
- Localization and
register sharing for predicate abstraction (with H. Jain, F. Ivancic, and M. K.
Ganai). In Proceedings of Tools and Algorithms for Construction and
Analysis of Systems (TACAS), April 2005.
- Efficient SAT-based
bounded model checking for software verification (with F. Ivancic, Z. Yang, M.
K. Ganai, and P. Ashar), in International Symposium on Leveraging
Applications of Formal Methods (ISoLA), November
2004.
SAT
Solvers and SMT Solvers
- Predicate Learning and
Selective Theory Deduction for a Difference Logic Solver (with C. Wang,
and M. K. Ganai). Design Automation Conference (DAC), July 2006.
- SDSAT: Tight Integration of
small domain encoding and lazy approaches in a separation logic solver
(with M. K. Ganai, and M. Talupur). In Proceedings of Tools and Algorithms
for the Construction and Analysis of Systems
(TACAS), March 2006.
- Deciding separation logic
formulae by SAT and incremental negative cycle elimination (with C. Wang,
F. Ivancic, and M. K. Ganai). In Proceedings of International
Conference on Logic for Artificial Intelligence and Reasoning (LPAR),
December 2005.
Hardware Verification using SAT Solvers
- Book: M. K. Ganai and A. Gupta.SAT-based
Scalable Formal Verification Solutions. Springer.
August 2007.
- M. Ganai and A. Gupta:
Completeness in SMT-based BMC for Software Programs. In Proceedings of the
International Conference of Design, Automation and Test in
- 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
- M. K. Ganai, A. Mukaiyama, A. Gupta, 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.
- SAT-based
Verification Methods and Applications in Hardware Verification (with M. K.
Ganai, and C. Wang). In School for Formal Methods
(SFM06:HV), May 2006.
- Beyond Safety: Customized SAT-based Model Checking (with M. K.
Ganai, and P. Ashar). In Proceedings of the ACM/IEEE
Design Automation Conference (DAC), June 2005.
- DiVer:
SAT-based Model Checking Platform for Large Scale Systems (with M. K. Ganai, and P.
Ashar). In Proceedings of Tools and Algorithms for Construction and
Analysis of Systems (TACAS), April 2005.
- Verification
of Embedded Memory Systems using Efficient Memory Modeling (with M. K. Ganai, and P. Ashar).In
Proceedings of the IEEE Design
Automation and Test Europe (DATE),
March 2005.
- A Survey of Recent Advances in
SAT-based Verification (with A. Biere, and M. R. Prasad). In International
Journal on Software Tools for Technology Transfer (STTT), Vol.
7(2):156—173, April 2005
.
- Lazy
Constraints and SAT Heuristics for Proof-based Abstraction (with M. K. Ganai, Z. Yang and P.
Ashar). In
Proceedings of the IEEE International Conference on VLSI Design, January
2005.
- Efficient
SAT-based Unbounded Model Checking Using Circuit Cofactoring
(with M. K. Ganai,
and P. Ashar).In Proceedings of the ACM/IEEE International Conference on
Computer-Aided Design (ICCAD), November 2004.
- Efficient
Modeling of Embedded Memories in Bounded Model Checking (with M. K. Ganai, and P. Ashar).In
Proceedings of the International Conference on Computer Aided Verification
(CAV), July 2004.
- Iterative Abstraction using
SAT-based BMC with Proof Analysis (with M. K. Ganai, Z. Yang, and P.
Ashar). In Proceedings of the ACM/IEEE International Conference on
Computer-Aided Design (ICCAD), November 2003.
- Abstraction and BDDs Complement SAT-based BMC in DiVer
(with C. Wang, M. K. Ganai, Z. Yang, P. Ashar). In Proceedings of the
International Conference on Computer Aided Verification (CAV), July 2003.
- Partition Based Decision Heuristics for Image
Computation Using SAT and BDDs (with Z. Yang, P.
Ashar, and L. Zhang). In Proceedings of the ACM/IEEE
International Conference on Computer-Aided Design (ICCAD), Nov. 2001.
- Dynamic Detection and Removal
of Inactive Clauses in SAT with Application in Image Computation (with
Anubhav Gupta, Z. Yang, and P. Ashar). In
Proceedings of the ACM/IEEE Design Automation Conference (DAC), June 2001.
- SAT-based Image Computation
with Application in Reachability Analysis (with
Z. Yang, P. Ashar, and Anubhav Gupta). In
Proceedings of the Conference on Formal Methods in Computer-Aided Design
(FMCAD), Nov. 2000.
- Integrating a Boolean Satisfiability Checker and BDDs
for Combinational Verification (with P. Ashar). In
Proceedings of the IEEE VLSI
Design Conference, Jan. 1998.
Design Specification and Verification in Electronic Design Automation
- Verification Languages (with A.
A. Bayazit, and Y. Mahajan). Invited article in the “The Industrial Information
Technology Handbook”, Ed. R. Zurawski, CRC Press, November
2004. Also printed in the Embedded Systems Handbook, Ed. R. Zurawski, CRC
Press, July 2005.
- Property-Specific Witness Graph Generation for
Guided Simulation (with A. E. Casavant, P.
Ashar, X. G. Liu, A. Mukaiyama, and K. Wakabayashi). In
Proceedings of the IEEE Conference on VLSI Design, January 2002.
- Fast Error Diagnosis for
Combinational Verification (with P. Ashar). In
Proceedings of the IEEE VLSI Design Conference, January 2000.
- Verification of Scheduling in the Presence of
Loops Using Uninterpreted Symbolic Simulation
(with P. Ashar, A. Raghunathan, and
- Exploiting Retiming in a Guided Simulation Based
Validation Methodology (with P. Ashar, and
- Toward Formalizing a Simulation Based Verification
Methodology (with P. Ashar and
- Using Complete-1-Distinguishability for FSM
equivalence checking (with P. Ashar and
Other Information
- (Old) Link to CMU: http://www.cs.cmu.edu/~guptaa
©2006 NEC Laboratories America, Inc. All rights reserved.