Department of Systems Analysis & Verification - PUBLICATIONS

NEC Laboratories America, Inc., Princeton Campus

Concurrency Analysis

• S. Kundu, M. K. Ganai, and A. Gupta, Partial Order Reduction for Scalable Testing of SystemC TLM Designs, in Proc. Design Automation Coference (DAC), June 8 - 13, 2008, Anaheim, CA, USA.
• 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.
• V. Kahlon. Parameterization as Abstraction: A Tractable Approach to the Dataflow Analysis of Concurrent Programs. Twenty Third Annual IEEE Symposium on Logic in Computer Science (LICS), Pittsburgh, USA. July 2008.
• S. Kundu, M. K. Ganai and R. Gupta. Partial Order Reduction for Scalable Testing of SystemC TLM Designs. Design Automation Conference, June 2008.
• V. Kahlon. Bootstrapping: A Technique for Scalable Flow and Context-Sensitive Pointer Alias Analysis. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Tucson, Arizona. June 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, 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.

F-Soft

• 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.
• 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.
• Malay K. Ganai, Aarti Gupta, Franjo Ivancic, Vineet Kahlon, Weihong Li, Nadia Papakonstantinou, Sriram Sankaranarayanan, and Chao Wang: Towards Precise and Scalable Verification of Embedded Software, In Proceedings of 2008 Design and Verification Conference (DVCon), San Jose, CA, February 2008.
• 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. 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, 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.
• F. Ivancic, I. Shlyakhter, A. Gupta, M. Ganai, V. Kahlon, C. Wang, Z. Yang. Model Checking C Programs Using F-Soft, in Proceedings of the International Conference on Computer Design (ICCD), October 2005.
• 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.
• F. Ivancic, Z. Yang, M. Ganai, A. Gupta, I. Shlyakhter, P. Ashar. F-Soft: Software Verification Platform, in Proceedings of the International Conference on Computer Aided Verification (CAV), July 2005.
• H. Jain, F. Ivancic, A. Gupta, M. Ganai. Localization and Register Sharing for Predicate Abstraction , in Proceedings of Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), April 2005.
• F. Ivancic, Z. Yang, M. Ganai, A. Gupta, P. Ashar. Efficient SAT-based Bounded Model Checking for Software Verification , Presented at International Symposium for Leveraging Applications of Formal Methods (ISoLA) 2004.

Dynamic Analyses

• 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
• Sriram Sankaranarayanan, Richard Chang, Guofei Jiang and Franjo Ivancic: State Space Exploration using Feedback Constraint Generation and Monte-Carlo Sampling. In Proceedings of ESEC/FSE, September 2007.

Hybrid Systems

• Sriram Sankaranarayanan, Thao Dang, and Franjo Ivancic: A Policy Iteration Technique for Computing Time-Elapse Using Template Polyhedra, Hybrid Systems: Computation and Control (HSCC 2008), April 2008
• Sriram Sankaranarayanan, Thao Dang, and Franjo Ivancic: Symbolic Model-Checking of Hybrid Systems using Template Polyhedra, Tools and Algorithms for Construction and Analysis of Systems (TACAS 2008), March 2008
• Sriram Sankaranarayanan, Henny B. Sipma and Zohar Manna: Fixed Point Iteration for Computing the Time-Elapse Operator. In Proceedings of HSCC, March 2006.

VeriSol

Books

• M. K. Ganai and A. Gupta. SAT-based Scalable Formal Verification Solutions. Springer Business Media. August 2007.

Papers

• M. K. Ganai and A. Gupta. Tunneling and Slicing: Towards Scalable BMC. Design Automation Conference, June 2008.
• 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.
• 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, 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.
• A. Gupta, M. K. Ganai, and C. Wang. SAT-based Verification Methods and Applications in Hardware Verification . In School for Formal Methods (SFM06:HV), LNCS Vol. 3965, May 2006.
• C. Wang, Z. Yang, F. Ivancic, and A. Gupta. Disjunctive Image Computation for Embedded Software Verification . In ACM Trans. on Design Automation of Electronic Systems. 12(2):10, April 2007 ACM Transactions on Design Automation of Electronic Systems (TODAES) 2008 Best Paper Award
• M. K. Ganai, M. Talupur, and A. Gupta, SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in a Separation Logic Solver , in TACAS '06. March 2006.
• C. Wang, Z. Yang, F. Ivancic, and A. Gupta, Disjunctive Image Computation for Embedded Software Verification , Design, Automation and Test in Europe (DATE'06). Munich, Germany. March 2006
• Chao Wang, Franjo Ivancic, Malay K. Ganai, Aarti Gupta Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination , in Proceedings of LPAR. Dec 2005.
• M. K. Ganai, A. Gupta, and P. Ashar. Beyond Safety: Customized SAT-based Model Checking , in Proceedings of DAC 2005.
• M. K. Ganai, A. Gupta, and P. Ashar. SAT-based Model Checking Platform for Large Scale Systems , in Proceedings of Conference on Tools and Algorithms for the 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 DATE, March 2005.
• A. Gupta, M. K. Ganai, P. Ashar, and Z. Yang, Lazy Constraints and SAT Heuristics for Proof-based Abstraction , in Proceedings of VLSI Design, January 2005.
• M. K. Ganai, A. Gupta, and P. Ashar, Efficient SAT-based Unbounded Model Checking Using Circuit Cofactoring , in Proceedings of ICCAD, November 2004.
• M. K. Ganai, A. Gupta, and P. Ashar, Efficient Modeling of Embedded Memories in Bounded Model Checking , in Proceedings of 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 ICCAD, November 2003.
• M. K. Ganai, A. Gupta, Z. Yang, and P. Ashar, Distributed SAT and Distributed Bounded Model Checking , in Proceedings of CHARME, September 2003.
• A. Gupta, M. K. Ganai, C. Wang, Z. Yang, and P.Ashar, Abstraction and BDDs Complement SAT-Based BMC in DiVer , in Proceedings of 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 DAC, June 2003.
• 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 DAC, June 2002.

SAT-based Verification

• Daijue Tang, Sharad Malik, Aarti Gupta, and C. Norris Ip: Symmetry Reduction in SAT-based Model Checking. In Proceedings of CAV, July 2005.
• Mukul R. Prasad, Armin Biere and Aarti Gupta: A Survey of Recent Advances in SAT-based Formal Verification. International Journal on Software Tools for Technology Transfer (STTT), Vol. 7(2):156--173, April 2005.
• Malay Ganai and Adnan Aziz: Improved SAT-based Bounded Reachability Analysis. In Proceedings of VLSI Design, 2002.
• Aarti Gupta, Zijiang Yang, Pranav Ashar, Lintao Zhang, and Sharad Malik: Partition-based Decision Heuristics for Image Computation using SAT and BDDs. In Proceedings of ICCAD, 2001.
• Aarti Gupta, Anubhav Gupta, Zijiang Yang, and Pranav Ashar: Dynamic Detection and Removal of Inactive Clauses in SAT with Application in Image Computation. In Proceedings of DAC, 2001.
• Aarti Gupta, Zijiang Yang, Pranav Ashar, and Anubhav Gupta: SAT-based Image Computation with Application in Reachability Analysis. In Proceedings of FMCAD, 2000.

Other

• Shantanu Gupta, Florin Sultan, Srihari Cadambi, Franjo Ivancic, and Martin Roetteler: RaceTM: Detecting Data Races using Transactional Memory, 20th ACM Symposium on Parallelism in Algorithms and Architectures (SPAA), Munich, Germany, June 2008 (short paper)
• Sriram Sankaranarayanan, Michael A. Colon, Henny B. Sipma, and Zohar Manna: Efficient Strongly Relational Polyhedral Analysis. In Proceedings of VMCAI, January 2006.
• C. Wang, B. Li, H. Jin, G. D. Hachtel and F. Somenzi. Improved Ariadne's Bundle by Following Multiple Threads in Abstraction Refinement. In IEEE Trans. on Computer-Aided Design (T-CAD),25(11):2297-2316, (2006).
• C. Wang, R. Bloem, K. Ravi, G. D. Hachtel and F. Somenzi. Compositional SCC analysis for Language Emptiness Checking. In Journal on Formal Methods in Systems Design. 28(1):5-26 (2006)
• B. Li, C. Wang and F. Somenzi. Abstraction Refinement in Symbolic Model Checking Using Satisfiability as the Only Decision Procedure. In Journal on Software Tools for Technology Transfer (STTT), 7(2):143-155 (2005).
• Aarti Gupta, Ali A. Bayazit and Yogesh Mahajan: Verification Languages. In The Industrial Information Technology Handbook, R. Zurawski (Ed.), CRC Press, 2005.