Himanshu Jain Computer Science Department Carnegie Mellon University Email: hjain [AT] cs [DOT] cmu [DOT] edu

[About | Research | Publications | Software | Coursework | Misc ]

• Building reliable software and hardware systems using techniques from model checking, static analysis, theorem proving, runtime verification, testing
• New solvers for propositional logic (SAT solvers), satisfiability modulo theory (SMT solvers)

• Verification Using Satisfiability Checking, Predicate Abstraction, and Craig Interpolation (pdf) (bibtex) (presentation)
  Himanshu Jain
  CMU CS technical report (CMU-CS-08-146).  

• Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
  Himanshu Jain, Edmund M. Clarke, Orna Grumberg.
  FMSD, To appear in Formal Methods in System Design
  
  
• Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog. (available online) (bibtex)
  Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund Clarke.
  IEEE TCAD 2008, In IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems.  
  
  
• Verification of SpecC using Predicate Abstraction. (available online) (bibtex)
  Edmund Clarke, Himanshu Jain, Daniel Kroening.
  FMSD 2007, Formal Methods in System Design.  

• Efficient SAT Solving for Non-Clausal Formulas using DPLL, Graphs, and Watched Cuts (pdf) (bibtex) (website)
  Himanshu Jain, Edmund M. Clarke.
  DAC 2009, To appear in 46th Design Automation Conference .
  
  
• Solver Technology for System-level to RTL Equivalence Checking (invited paper)
  Alfred Koelbl, Reily Jacoby, Himanshu Jain, Carl Pixley
  DATE 2009, To appear in Design, Automation and Test in Europe .
  
  
• Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations (ps) (pdf) (conference presentation) (bibtex) (experimental data)
  Himanshu Jain, Edmund M. Clarke, Orna Grumberg.
  CAV 2008, In 20th International Conference on Computer Aided Verification
  Preliminary version available as CMU CS technical report (CMU-CS-08-102).   (pdf) (bibtex)
  Among selected papers of CAV 2008 conference. Invited for journal publication.
  
  
• VCEGAR: Verilog CounterExample Guided Abstraction Refinement. (tool description ) (ps) (pdf) (bibtex)
  Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund Clarke.
  TACAS 2007, 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.
  
  
• Satisfiability Checking of Non-clausal Formulas using General Matings. (ps) (pdf) (conference presentation) (bibtex)
  Himanshu Jain, Constantinos Bartzis, Edmund Clarke.
  SAT 2006, Ninth International Conference on Theory and Applications of Satisfiability Testing .
  Extended version (ps) (pdf)
  
  
• Using Statically Computed Invariants inside the Predicate Abstraction and Refinement Loop. (ps) (pdf) (conference presentation) (bibtex)
  Himanshu Jain, Franjo Ivančić, Aarti Gupta, Ilya Shlyakhter, Chao Wang.
  CAV 2006, 18th Computer-aided Verification .
  
  
• Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog. (ps) (pdf) (conference presentation) (bibtex)
  Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund Clarke.
  DAC 2005, 42nd Design Automation Conference .
  Nominated for DAC 2005 best paper award.
  
  
• Localization and Register Sharing for Predicate Abstraction. (ps) (pdf) (conference presentation) (bibtex)
  Himanshu Jain, Franjo Ivančić, Aarti Gupta, Malay Ganai.
  TACAS 2005, Eleventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems.
  
  
• Verification of SpecC using Predicate Abstraction. (ps) (pdf) (conference presentation) (bibtex)
  Himanshu Jain, Daniel Kroening, Edmund Clarke.
  MEMOCODE 2004, Second ACM-IEEE International Conference on Formal Methods and models for Codesign.
  Among the three best papers of the conference. Invited for journal publication.
  

• SAT Solver Descriptions: CMUSAT-Base and CMUSAT. (ps) (pdf)
  Himanshu Jain, Edmund Clarke.
  In SAT competition 2007.
  
  
• Optimized CNF Encoding for Sudoku Puzzles. (short paper )
  Gihwon Kwon, Himanshu Jain.
  In 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2006).
  
  
• Model Checking: Back and Forth Between Hardware and Software. (pdf)
   Edmund Clarke, Anubhav Gupta, Himanshu Jain, and Helmut Veith.
  In IFIP Working Conference on Verified Software: Theories, Tools, Experiments (VSTTE 2005).
  
  
• Grand Challenge: Model Check Software (invited paper).
  Edmund Clarke, Himanshu Jain, Nishant Sinha.
  In workshop on Verification of Infinite-State Systems with Applications to Security (VISSAS 2005).

• Predicate Abstraction and Refinement Techniques for Verifying Verilog. Edmund Clarke, Himanshu Jain, Daniel Kroening. CMU-CS-04-139. (ps) (pdf).     
• Decomposition-based Symbolic Model Checking for Liveness properties. B.Tech Thesis 2003, Dept. of Computer Science and Engineering, IIT Bombay. (ps), presentation (ps), (pdf)
  
•  Automata on Infinite Objects (survey). Junior thesis report 2002,  Dept. of Computer Science and Engineering, IIT Bombay.  (ps), presentation (ps), (pdf)

• NFLSAT: A new non-clausal SAT solver based on DPLL and NNF.
• VCEGAR: performs word level predicate abstraction and refinement for verifying RTL Verilog programs. 
• SatMate: A new non-clausal SAT solver.

• Bug Catching: Automated Program Verification and Testing (15-414, Fall 2006) (course webpage) 
• Algorithms (15-451, Spring 2005) (course webpage)

• Pointer Analysis for CASH Compiler Framework, Optimizing Compilers, Spring 2005. (project webpage)
• Automatically Fixing User/Kernel Pointer Bugs, Secure Software Systems, Fall 2004.
  
• Static Reachability Analysis of IP Networks, Computer Networks, Fall 2004. 
  

• Upcoming Conferences
• The Gigascale Systems Research Center