Himanshu Jain Computer Science Department Carnegie Mellon University Email: hjain [AT] cs [DOT] cmu [DOT] edu Office address: Wean Hall 4112 Computer Science Department Carnegie Mellon University 5000 Forbes Avenue Pittsburgh, PA - 15213 Phone : 1-412-268-3047

[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)
• Programming language support for concurrency, software and hardware transactional memory

• Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog. (available online) (bibtex)
  Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund Clarke.
  IEEE TCAD 2007, To appear 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 Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
  Himanshu Jain, Edmund M. Clarke, Orna Grumberg.
  CAV 2008, To appear in 20th International Conference on Computer Aided Verification
  Preliminary version available as CMU CS technical report (CMU-CS-08-102).   (pdf) (bibtex)
  
  
• 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)

• CMUSAT and CMUSAT-Base: New CNF SAT solvers (coming soon).
• 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