Systems Analysis & Verification

All Publications by Year

2009

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

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

V. Kahlon, N. Sinha, Y. Zhang and E. Kruus: Static Data Race Detection for Concurrent Programs with Asynchronous Calls. The 7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), Amsterdam, The Netherlands. August 2009.

V. Kahlon. Boundedness vs. Unboundedness of Lock Chains: Characterizing Decidability of CFL-Reachability for Threads Communicating via Locks. LICS 2009, Los Angeles. August 2009.

Malay K. Ganai and Sudipta Kundu. Reduction of Verification Conditions for Concurrent System using Mutually Atomic Transactions. SPIN, Grenoble, France. July 2009.

Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, and Chao Wang: Automatic Discovery of Transition Symmetry in Multithreaded Programs using Dynamic Analysis. SPIN, Grenoble, France. July 2009.

Vineet Kahlon, Chao Wang, and Aarti Gupta: Monotonic Partial Order Reduction CAV 2009.

Vineet Kahlon, Sriram Sankaranarayanan, and Aarti Gupta: Semantic Reduction of Thread Interleavings in Concurrent Programs. S. Kowalewski and A. Philippou (Eds.): TACAS 2009, LNCS 5505, pp. 124–138, 2009., c Springer-Verlag Berlin Heidelberg 2009.

R. Chang, G. Jiang, F. Ivancic, S. Sankaranarayanan, and V. Shmatikov Inputs of Coma: Static Detection of Denial-of-Service Vulnerabilities, 22nd IEEE Computer Security Foundations Symposium (CSF22), Port Jefferson, NY, July 2009.

S. Gupta, F. Sultan, S. Cadambi, F. Ivancic, and M. Roetteler. Using Hardware Transactional Memory for Data Race Detection, 23rd IEEE International Parallel and Distributed Processing Symposium (IPDPS), Rome, Italy, May 2009.

Malay K. Ganai and Franjo Ivancic. Efficient Decision Procedure for Non-linear Arithmetic Constraints using CORDIC., FMCAD, Austin, TX. Nov 2009.

A. Kanade, R. Alur, F. Ivancic, S. Ramesh, S. Sankaranarayanan and K.C. Shashishar: Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models, 21st International Conference on Computer-Aided Verification (CAV), Grenoble, France, July 2009.

Malay K. Ganai and Franjo Ivancic. Efficient Decision Procedure for Non-linear Arithmetic Constraints using CORDIC., FMCAD, Austin, TX. Nov 2009.

A. Kanade, R. Alur, F. Ivancic, S. Ramesh, S. Sankaranarayanan and K.C. Shashishar: Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models, 21st International Conference on Computer-Aided Verification (CAV), Grenoble, France, July 2009.

Franjo Ivancic, Sriram Sankaranarayanan, Aarti Gupta and Ilya Shlyakhter, Buffer Overflow Analysis using Environment Refinement, Draft [PDF]

2008

N. Sinha, Symbolic Program Analysis Using Term Rewriting and Generalization, In Proceedings of the International Conference on Formal Methods in Computer Aided Design (FMCAD), November 2008, Portland, OR, USA. [Slides]

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

M. K. Ganai and A. Gupta. Efficient Modeling of Concurrent Systems in BMC. 15th International SPIN Workshop on Model Checking of Software (SPIN). August 10-12, 2008, Los Angeles, USA. [ Slides ]

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

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 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, Tunneling and Slicing: Towards Scalable BMC. In Proc. Design Automation Coference (DAC), June 8 - 13, 2008, Anaheim, CA, USA.

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.

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, Franjo Ivancic, and Aarti Gupta: Mining Library Specifications Using Inductive Logic Programming, Intl. Conference on Software Engg. (ICSE), May 2008

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

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.

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.

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.


2007

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

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

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

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.

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.

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


2006

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.

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.

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.

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.

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.

Sriram Sankaranarayanan, Henny B. Sipma and Zohar Manna: Fixed Point Iteration for Computing the Time-Elapse Operator. In Proceedings of HSCC, March 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 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

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)

Sriram Sankaranarayanan, Michael A. Colon, Henny B. Sipma, and Zohar Manna: Efficient Strongly Relational Polyhedral Analysis. In Proceedings of VMCAI, January 2006.


2005

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

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.

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.

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.


2004

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.

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.

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.


2003

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.


2002

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.

Malay Ganai and Adnan Aziz: Improved SAT-based Bounded Reachability Analysis. In Proceedings of VLSI Design, 2002.


2001

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.


2000

Aarti Gupta, Zijiang Yang, Pranav Ashar, and Anubhav Gupta: SAT-based Image Computation with Application in Reachability Analysis. In Proceedings of FMCAD, 2000.