 |
Systems Analysis & Verification
VeriSol Publications
Books
M. K. Ganai and A. Gupta.
SAT-based Scalable Formal Verification Solutions. Springer Business Media. August 2007.
Papers
2008
M. K. Ganai.
Efficient Decision Procedures For Bounded Integer Non-linear Operations Using SMT(LIA).
4th Haifa Verification Conference (HVC), Oct 28-30, Haifa, Israel.
[Slides]
M. K. Ganai and W. Li.
D-TSR: Parallelizing SMT-based BMC using Tunnels over a Distributed Framework.
4th Haifa Verification Conference (HVC), Oct 28-30, Haifa, Israel.
[Slides]
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.
[Slides]
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.
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.
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.
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
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.
2004
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.
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.
Publications in Other Areas:
|
