NEC

NEC Laboratories America, Inc.

Aarti Gupta

NEC Laboratories America, Inc.

4 Independence Way, Suite 200

Princeton, NJ 08520

(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

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) August 10-12, 2008, Los Angeles, USA.
  • 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), June 8 - 13, 2008, Anaheim, CA, USA.
  • 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, I. Shlyakhter, and A. Gupta. Static Analysis in Disjunctive Numerical Domains. In Proceedings of the International Static Analysis Symposium (SAS), August 2006.
  • A. Zaks, I. Shlyakhter, F. Ivancic, 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.
  • H. Jain, F. Ivancic, I. Shlyakhter, C. Wang and A. Gupta. Using statically computed invariants inside the predicate abstraction and refinement loop. Computer Aided Verification (CAV), August 2006.
  • 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 Europe (DATE), March 2006.
  • F. Ivancic, I. Shlyakhter, A. Gupta, M. Ganai, 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-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.
  • Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver (with M. K. Ganai, L. Zhang, P. Ashar, and S. Malik ). In Proceedings of the ACM/IEEE Design Automation Conference (DAC), June 2002.

 

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 Europe, March 2008.
  • 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. 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.
  • Symmetry Reduction in SAT-based Model Checking (with D. Tang, S. Malik , and C. N. Ip). In Proceedings of International Conference on Computer Aided Verification (CAV), July 2005
  • 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.
  • Efficient Distributed SAT and SAT-based Distributed Bounded Model Checking (with M. K. Ganai, Z. Yang, and P. Ashar). In Proceedings of the Conference on Correct Hardware Designs and Verification Methods (CHARME), September 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.
  • Learning from BDDs in SAT-based Bounded Model Checking (with M. K. Ganai, C. Wang, Z. Yang, and P. Ashar). In Proceedings of the ACM/IEEE Design Automation Conference (DAC), June 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.
  • Assertion-based Verification Turns the Corner. In IEEE Design & Test of Computers, Volume 19, No. 4, 2002.
  • 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 S. Bhattacharya ). In Proceedings of the IEEE International Conference on Computer Design (ICCD), October 1999.
  • Exploiting Retiming in a Guided Simulation Based Validation Methodology (with P. Ashar, and S. Malik ). In Proceedings of the Conference on Correct Hardware Design and Verification Methods (CHARME), September 1999.
  • Toward Formalizing a Simulation Based Verification Methodology (with P. Ashar and S. Malik ). In Proceedings of the ACM/IEEE Design Automation Conference (DAC), June 1997.
  • Using Complete-1-Distinguishability for FSM equivalence checking (with P. Ashar and  S. Malik ). In Proceedings of the ACM/IEEE International Conference on Computer-Aided Design (ICCAD), June 1996. (A journal version appeared in the ACM Transactions on Design Automation of Electronic Systems. 

Other Information

 NEC Laboratories America Home

©2006 NEC Laboratories America, Inc. All rights reserved.