Conferences and Journals:

• S. Iyer, D. Sahoo, E. A. Emerson, J. Jain. On Partitioning and Symbolic Model Checking, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, TCAD, Vol. 25, No. 5, May 2006 [PDF]


• D. Sahoo, J. Jain, S. Iyer, D. Dill, E. A. Emerson. Predictive Reachability using a Sample-based Approach, In Proceedings of the 13th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, CHARME 2005, LNCS 3725, pp. 388-392, Saarbrücken, Germany, October 3-6, 2005 [PDF]


• S. Iyer, D. Sahoo, J. Jain, M. Prasad, T. Sidle. Error detection using BMC in a parallel environment, In Proceedings of the 13th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, CHARME 2005, LNCS 3725, pp. 354-358, Saarbrücken, Germany, October 3-6, 2005 [PDF]


• D. Sahoo, J. Jain, S. Iyer, D. Dill. A new Reachability Algorithm for Symmetric Multi-processor Architecture, In Proceedings of the Third International Symposium on Automated Technology for Verification and Analysis, ATVA 2005, LNCS 3707, pp. 26-38, Taipei, Taiwan, October 4-7, 2005 [PDF]


• S. Iyer, J. Jain, D. Sahoo, E. A. Emerson. Under-approximation heuristics for Grid-based BMC, In Proceedings of the 4th International Workshop on Parallel and Distributed Methods in Verification, PDMC 2005, ENTCS, Vol. 135, Issue 2, pp. 1-80, Lisbon, Portugal 10 July 2005 [Web] [PDF] [PPT]


• S. Iyer, D. Sahoo, E. A. Emerson, J. Jain. On Partitioning and Symbolic Model Checking, In Proceedings of Formal Methods, International Symposium of Formal Methods Europe, LNCS 3582 pp. 497-511, Newcastle, UK, July 18-22, 2005 [PDF] [PPT]


• D. Sahoo, J. Jain, S. Iyer, D. Dill, E. A. Emerson. Multi-threaded Reachability, In Proceedings of the 42nd Design Automation Conference, DAC 2005, pp. 467-470, San Diego, CA, USA, June 13-17, 2005 [PDF] [PPT]


• D. Sahoo, S. Iyer, J. Jain, C. Stangier, A. Narayan, D. Dill, E. A. Emerson. A Partitioning Methodology for BDD-based Verification, In Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2004, LNCS 3312, pp. 399-413, Austin, USA, November 14-17, 2004 [PDF]


• S. Iyer D. Sahoo, C. Stangier, A. Narayan, J. Jain. Improved Symbolic Verification using Partitioning Techniques, In Proceedings of the 12th IFIP Advanced Research Working Conference on Correct Hardware Design and Verification Methods, CHARME 2003, LNCS 2860, pp. 410-424, L'Aquila, Italy, October 21-24, 2003 [PDF]


• C. Puchol, S. Iyer. The MacBeth Specification, Modeling and Programming Language, In Proceedings of the IEEE Real Time Technology and Applications Symposium, pp. 181-190, Taipei, Taiwan, May 31-June 2, 2001. [PDF]

• S. Iyer, J. Jain, D. Sahoo, T. Shimuzu. Verification of Industrial Designs Using a Computing Grid With More than 100 Nodes, In Industry Session at Asian Test Symposium 2005. [PDF]


• D. Sahoo, J. Jain, S. Iyer, D. Dill. A new Reachability Algorithm for Symmetric Multi-processor Architecture, In Formal Equivalence and Assertion-based Verification Workshop 2005 [PPT]


• S. Iyer, D. Sahoo, E. A. Emerson, J. Jain. A new algorithm for partitioned model checking, In Proceedings of the 14th IEEE/ACM International Workshop on Logic & Synthesis, IWLS 2005, Lake Arrowhead, USA, June 8-10, 2005.


• D. Sahoo, J. Jain, S. Iyer, C. Stangier, A. Narayan, D. Dill, E. A. Emerson. A Partitioning Methodology for BDD-based Verification, In Proceedings of the 13th IEEE/ACM International Workshop on Logic & Synthesis, pp. 192-199, Temecula, USA, June 2-4, 2004.


• S. Iyer C. Stangier, D. Sahoo, A. Narayan, J. Jain. Using Partitioned-OBDDs for Efficient Symbolic Model Checking, In Proceedings of the 12th IEEE/ACM International Workshop on Logic & Synthesis, pp. 236-243, Laguna Beach, USA, May 28-30, 2003

• [UT-CS] Efficient and Effective Symbolic Model Checking. The University of Texas at Austin, Department of Computer Sciences. Dissertation, Advisor: Prof. E. A. Emerson December 2006. [PDF]
  
• [UT-CS] Efficient and Effective Symbolic Model Checking. The University of Texas at Austin, Department of Computer Sciences. Dissertation Proposal, Advisor: Prof. E. A. Emerson October 26, 2003. [PDF]
  
• [IITB-CSE] Verification of Synchronous Programs with Resource Constraints. Indian Institute of Technology, Bombay; Computer Science and Engineering Department. B. Tech. Project Report, April 1999. [PDF]

• 6904578 System and method for verifying a plurality of states associated with a target circuit
• 7028279 Circuit verification
• 7032197 System and method for executing image computation associated with a target circuit

• 20040093541 System and method for evaluating an erroneous state associated with a target circuit
• 20040199887 Determining one or more reachable states in a circuit using distributed computing and one or more partitioned data structures