Publications

See the full list of publications at the 

  • S. Sohail and F. Somenzi. A two-stage algorithm for LTL games. In Ninth International Conference on Formal Methods in Computer-Aided Design (FMCAD 2009), pages 77–84, Austin, TX, November 2009.
  • K. Nanshi and F. Somenzi. Constraints in one-to-many concretization for abstraction refinement. In Proceedings of the Design Automation Conference, pages 569–574, San Francisco, CA, July 2009.
  • H. Kim and F. Somenzi. Efficient term-ITE conversion for satisfiability modulo theories. In Twelfth International Conference on Theory and Applications of Satisfiability Testing (SAT 2009), pages 195–208, Swansea, UK, June 2009. Springer-Verlag. LNCS 5584.
  • H. Han and F. Somenzi. On-the-fly clause improvement. In Twelfth International Conference on Theory and Applications of Satisfiability Testing (SAT 2009), pages 209–222, Swansea, UK, June 2009. Springer-Verlag. LNCS 5584.
  • H. Kim, H. Jin, K. Ravi, P. Spacek, J. Pierce, R. P. Kurshan, and F. Somenzi. Application of formal word-level analysis to constrained random simulation. In Twentieth Conference on Computer Aided Verification (CAV’08), pages 487–490, Princeton, NJ, July 2008. LNCS 5123.
  • K. Nanshi and F. Somenzi. Improved visibility in one-to-many trace concretization. In Design Automation and Test in Europe, pages 819–824, Munich, Germany, March 2008.
  • S. Sohail, F. Somenzi, and K. Ravi. A hybrid algorithm for LTL games. In Verification, Model Checking and Abstract Interpretation, pages 309–323, San Francisco, CA, January 2008. LNCS 4905.
  • H. Kim, H. Jin, and F. Somenzi. Disequality management in integer difference logic via finite instantiations. Journal on Satisfiability, Boolean Modeling and Computation, 3:47–66, 2007.
  • H. Han and F. Somenzi. Alembic: An efficient algorithm for CNF pre-processing. In Proceedings of the Design Automation Conference, pages 582–587, San Diego, CA, June 2007.
  • D. Ward and F. Somenzi. Decomposing image computation for symbolic reachability analysis using control flow information. In Proceedings of the International Conference on Computer-Aided Design, pages 779–785, San Jose, CA, November 2006.
  • H. Kim and F. Somenzi. Finite instantiations for integer difference logic. In Formal Methods in Computer Aided Design (FMCAD’06), pages 31–38, San Jose, CA, November 2006.
  • M. Awedh and F. Somenzi. Automatic invariant strengthening to prove properties in bounded model checking. In Proceedings of the Design Automation Conference, pages 1073–1076, San Francisco, CA, July 2006.
  • K. Nanshi and F. Somenzi. Guiding simulation with increasingly refined abstract traces. In Proceedings of the Design Automation Conference, pages 737–742, San Francisco, CA, July 2006.
  • C. Wang, G. D. Hachtel, and F. Somenzi. Abstraction Refinement for Large Scale Model Checking. Springer, 2006.
  • C. Wang, B. Li, H. Jin, G. D. Hachtel, and F. Somenzi. Fine-grain abstraction and SOR guided refinement for large scale model checking. IEEE Transactions on Computer-Aided Design of Integrated Circuits, 25(11):2297–2316, 2006.
  • C. Wang, R. Bloem, K. Ravi, G. D. Hachtel, and F. Somenzi. Compositional SCC analysis for language emptiness checking. Journal of Formal Methods in System Design, 28(1):5–26, 2006.
  • A. Kuehlmann and F. Somenzi. Equivalence checking. In L. Scheffer, L. Lavagno, and G. Martin, editors, Electronic Design Automation for Integrated Circuits Handbook. CRC Press, 2006.
  • B. Li and F. Somenzi. Efficient abstraction refinement in interpolation-based unbounded model checking. In International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS’06), pages 227–241, Vienna, Austria, March 2006. LNCS 3920.
  • H. Jin and F. Somenzi. Strong conflict analysis for propositional satisfiability. In Design, Automation and Test in Europe (DATE’06), pages 818–823, Munich, Germany, March 2006.
  • R. Bloem, H. N. Gabow, and F. Somenzi. An algorithm for strongly connected component analysis in n log n symbolic steps. Formal Methods in System Design, 28(1):37–56, January 2006.
  • D. Ward and F. Somenzi. Automatic generation of hints for symbolic traversal. In Correct Hardware Design and Verification Methods (CHARME’05), pages 207–221, Saarbrucken, Germany, October 2005. Springer-Verlag. LNCS 3725.
  • M. Awedh and F. Somenzi. Termination criteria for bounded model checking: Extensions and comparison. Electronic Notes in Theoretical Computer Science, 144(1):51–66, 2006. Presented at the Third International Workshop on Bounded Model Checking (BMC’05).
  • H. Jin and F. Somenzi. Prime clauses for fast enumeration of satisfying assignments to Boolean circuits. In Proceedings of the Design Automation Conference, pages 750–753, Anaheim, CA, June 2005.
  • H. Jin, H. Han, and F. Somenzi. Efficient conflict analysis for finding all satisfying assignments of a Boolean circuit. In International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS’05), pages 287–300, April 2005. LNCS 3440.
  • B. Li, C. Wang, and F. Somenzi. Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure. Software Tools for Technology Transfer, 7(2):143–155, April 2005.