Enhancing Simulation with BDDs and ATPG. - Malay K. Ganai; Adnan Aziz; Andreas Kuehlmann (DAC, 1999)

Performance Driven Synthesis for Pass-Transistor Logic. - Tai-Hung Liu; Malay K. Ganai; Adnan Aziz; Jeffrey L. Burns (VLSI Design, 1999)

Circuit-based Boolean Reasoning. - Andreas Kuehlmann; Malay K. Ganai; Viresh Paruthi (DAC, 2001)

Rarity based guided state space search. - Malay K. Ganai; Adnan Aziz (ACM Great Lakes Symposium on VLSI, 2001)

SIVA: A System for Coverage-Directed State Space Search. - Malay K. Ganai; Praveen Yalagandula; Adnan Aziz; Andreas Kuehlmann; Vigyan Singhal (J. Electron. Test., 2001)

Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver. - Malay K. Ganai; Pranav Ashar; Aarti Gupta; Lintao Zhang; Sharad Malik (DAC, 2002)

Improved SAT-Based Bounded Reachability Analysis. - Malay K. Ganai; Adnan Aziz (ASP-DAC/VLSI Design, 2002)

Robust Boolean reasoning for equivalence checking and functional property verification. - Andreas Kuehlmann; Viresh Paruthi; Florian Krohm; Malay K. Ganai (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2002)

Abstraction and BDDs Complement SAT-Based BMC in DiVer. - Aarti Gupta; Malay K. Ganai; Chao Wang 001; Zijiang Yang 006; Pranav Ashar (CAV, 2003)

Learning from BDDs in SAT-based bounded model checking. - Aarti Gupta; Malay K. Ganai; Chao Wang 001; Zijiang Yang 006; Pranav Ashar (DAC, 2003)

Iterative Abstraction using SAT-based BMC with Proof Analysis. - Aarti Gupta; Malay K. Ganai; Zijiang Yang 006; Pranav Ashar (ICCAD, 2003)

Efficient Modeling of Embedded Memories in Bounded Model Checking. - Malay K. Ganai; Aarti Gupta; Pranav Ashar (CAV, 2004)

Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. - Malay K. Ganai; Aarti Gupta; Pranav Ashar (ICCAD, 2004)

F-Soft: Software Verification Platform. - Franjo Ivancic; Zijiang Yang 006; Malay K. Ganai; Aarti Gupta; Ilya Shlyakhter; Pranav Ashar (CAV, 2005)

Beyond safety: customized SAT-based model checking. - Malay K. Ganai; Aarti Gupta; Pranav Ashar (DAC, 2005)

Verification of Embedded Memory Systems using Efficient Memory Modeling. - Malay K. Ganai; Aarti Gupta; Pranav Ashar (DATE, 2005)

Model Checking C Programs Using F-SOFT. - Franjo Ivancic; Ilya Shlyakhter; Aarti Gupta; Malay K. Ganai; Vineet Kahlon; Chao Wang 001; Zijiang Yang 006 (ICCD, 2005)

Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination. - Chao Wang 001; Franjo Ivancic; Malay K. Ganai; Aarti Gupta (LPAR, 2005)

DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems. - Malay K. Ganai; Aarti Gupta; Pranav Ashar (TACAS, 2005)

Localization and Register Sharing for Predicate Abstraction. - Himanshu Jain; Franjo Ivancic; Aarti Gupta; Malay K. Ganai (TACAS, 2005)

Lazy Constraints and SAT Heuristics for Proof-Based Abstraction. - Aarti Gupta; Malay K. Ganai; Pranav Ashar (VLSI Design, 2005)

Predicate learning and selective theory deduction for a difference logic solver. - Chao Wang 001; Aarti Gupta; Malay K. Ganai (DAC, 2006)

Accelerating high-level bounded model checking. - Malay K. Ganai; Aarti Gupta (ICCAD, 2006)

SAT-Based Verification Methods and Applications in Hardware Verification. - Aarti Gupta; Malay K. Ganai; Chao Wang 001 (SFM, 2006)

SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in a Separation Logic Solver. - Malay K. Ganai; Muralidhar Talupur; Aarti Gupta (TACAS, 2006)

Efficient distributed SAT and SAT-based distributed Bounded Model Checking. - Malay K. Ganai; Aarti Gupta; Zijiang Yang 006; Pranav Ashar (Int. J. Softw. Tools Technol. Transf., 2006)

Efficient BMC for Multi-Clock Systems with Clocked Specifications. - Malay K. Ganai; Aarti Gupta (ASP-DAC, 2007)

Synthesizing "Verification Aware" Models: Why and How? - Malay K. Ganai; Akira Mukaiyama; Aarti Gupta; Kazutoshi Wakabayashi (VLSI Design, 2007)

SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in Solving Difference Logic. - Malay K. Ganai; Muralidhar Talupur; Aarti Gupta (J. Satisf. Boolean Model. Comput., 2007)

SAT-Based Scalable Formal Verification Solutions - Malay K. Ganai; Aarti Gupta (Springer, 2007)

Tunneling and slicing: towards scalable BMC. - Malay K. Ganai; Aarti Gupta (DAC, 2008)

Partial order reduction for scalable testing of systemC TLM designs. - Sudipta Kundu; Malay K. Ganai; Rajesh Gupta 001 (DAC, 2008)

Completeness in SMT-based BMC for Software Programs. - Malay K. Ganai; Aarti Gupta (DATE, 2008)

Efficient Decision Procedure for Bounded Integer Non-linear Operations Using SMT(). - Malay K. Ganai (Haifa Verification Conference, 2008)

d-TSR: Parallelizing SMT-Based BMC Using Tunnels over a Distributed Framework. - Malay K. Ganai; Weihong Li (Haifa Verification Conference, 2008)

Embedded software verification: challenges and solutions. - Chao Wang 001; Malay K. Ganai; Shuvendu K. Lahiri; Daniel Kroening (ICCAD, 2008)

PED: Proof-Guided Error Diagnosis by Triangulation of Program Error Causes. - Gogul Balakrishnan; Malay K. Ganai (SEFM, 2008)

Efficient Modeling of Concurrent Systems in BMC. - Malay K. Ganai; Aarti Gupta (SPIN, 2008)

Bitwidth Reduction via Symbolic Interval Analysis for Software Model Checking. - Aleksandr Zaks; Zijiang Yang 006; Ilya Shlyakhter; Franjo Ivancic; Srihari Cadambi; Malay K. Ganai; Aarti Gupta; Pranav Ashar (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2008)

Efficient SAT-based bounded model checking for software verification. - Franjo Ivancic; Zijiang Yang 006; Malay K. Ganai; Aarti Gupta; Pranav Ashar (Theor. Comput. Sci., 2008)

Symbolic Predictive Analysis for Concurrent Programs. - Chao Wang 001; Sudipta Kundu; Malay K. Ganai; Aarti Gupta (FM, 2009)

Efficient decision procedure for non-linear arithmetic constraints using CORDIC. - Malay K. Ganai; Franjo Ivancic (FMCAD, 2009)

Bang for the buck: Improvising and scheduling verification engines for effective resource utilization. - Malay K. Ganai; Weihong Li (MEMOCODE, 2009)

Reduction of Verification Conditions for Concurrent System Using Mutually Atomic Transactions. - Malay K. Ganai; Sudipta Kundu (SPIN, 2009)

Contessa: Concurrency Testing Augmented with Symbolic Analysis. - Sudipta Kundu; Malay K. Ganai; Chao Wang 001 (CAV, 2010)

Scalable and precise program analysis at NEC. - Gogul Balakrishnan; Malay K. Ganai; Aarti Gupta; Franjo Ivancic; Vineet Kahlon; Weihong Li; Naoto Maeda; Nadia Papakonstantinou; Sriram Sankaranarayanan 001; Nishant Sinha 001; Chao Wang 001 (FMCAD, 2010)

Propelling SAT and SAT-based BMC using careset. - Malay K. Ganai (FMCAD, 2010)

Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. - Sicun Gao; Malay K. Ganai; Franjo Ivancic; Aarti Gupta; Sriram Sankaranarayanan 001; Edmund M. Clarke (FMCAD, 2010)

Efficient state space exploration: Interleaving stateless and state-based model checking. - Malay K. Ganai; Chao Wang 001; Weihong Li (ICCAD, 2010)

Numerical stability analysis of floating-point computations using software model checking. - Franjo Ivancic; Malay K. Ganai; Sriram Sankaranarayanan 001; Aarti Gupta (MEMOCODE, 2010)

Interval Analysis for Concurrent Trace Programs Using Transaction Sequence Graphs. - Malay K. Ganai; Chao Wang 001 (RV, 2010)

Trace-Based Symbolic Analysis for Atomicity Violations. - Chao Wang 001; Rhishikesh Limaye; Malay K. Ganai; Aarti Gupta (TACAS, 2010)

Scalable and precise symbolic analysis for atomicity violations. - Malay K. Ganai (ASE, 2011)

BEST: A symbolic testing tool for predicting multi-threaded program failures. - Malay K. Ganai; Nipun Arora; Chao Wang 001; Aarti Gupta; Gogul Balakrishnan (ASE, 2011)

Predicting Concurrency Failures in the Generalized Execution Traces of x86 Executables. - Chao Wang 001; Malay K. Ganai (RV, 2011)

Symbolic predictive analysis for concurrent programs. - Chao Wang 001; Sudipta Kundu; Rhishikesh Limaye; Malay K. Ganai; Aarti Gupta (Formal Aspects Comput., 2011)

Dynamic Livelock Analysis of Multi-threaded Programs. - Malay K. Ganai (RV, 2012)

DTAM: dynamic taint analysis of multi-threaded programs for relevancy. - Malay K. Ganai; Dongyoon Lee; Aarti Gupta (SIGSOFT FSE, 2012)

Efficient data race prediction with incremental reasoning on time-stamped lock history. - Malay K. Ganai (ASE, 2013)

SETSUDŌ: perturbation-based testing framework for scalable distributed systems. - Pallavi Joshi; Malay K. Ganai; Gogul Balakrishnan; Aarti Gupta; Nadia Papakonstantinou (TRIOS@SOSP, 2013)

ReproLite: A Lightweight Tool to Quickly Reproduce Hard System Bugs. - Kaituo Li; Pallavi Joshi; Aarti Gupta; Malay K. Ganai (SoCC, 2014)

Environment-Sensitive Performance Tuning for Distributed Service Orchestration. - Yu Lin; Franjo Ivancic; Pallavi Joshi; Gogul Balakrishnan; Malay K. Ganai; Aarti Gupta (VECPAR, 2014)